mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case mp
c w : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
hw : w ∈ circleMap c R '' Ioc 0 (2 * π)
⊢ ¬IntervalIntegrable (fun θ ↦ (circleMap 0 R θ * I) • (circleMap c R θ - w) ^ n) volume 0 (2 * π)

Tactic:
rcases hw with ⟨θ, hθ, rfl⟩

Goal state after:
case mp
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ Ioc 0 (2 * π)
⊢ ¬IntervalIntegrable (fun θ_1 ↦ (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n) volume 0 (2 * π)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h_int : IntervalIntegrable g volume 0 T
hT : 0 < T
t : ℝ
h'_int : ∀ (a₁ a₂ : ℝ), IntervalIntegrable g volume a₁ a₂ := intervalIntegrable₀ hg (LT.lt.ne' hT) h_int
ε : ℝ := Int.fract (t / T) * T
⊢ ∫ (x : ℝ) in 0..t, g x ≤ sSup ((fun t ↦ ∫ (x : ℝ) in 0..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0..T, g x

Tactic:
conv_lhs =>
    rw [← Int.fract_div_mul_self_add_zsmul_eq T t hT.ne', ←
      integral_add_adjacent_intervals (h'_int 0 ε) (h'_int _ _)]

Goal state after:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h_int : IntervalIntegrable g volume 0 T
hT : 0 < T
t : ℝ
h'_int : ∀ (a₁ a₂ : ℝ), IntervalIntegrable g volume a₁ a₂ := intervalIntegrable₀ hg (LT.lt.ne' hT) h_int
ε : ℝ := Int.fract (t / T) * T
⊢ (∫ (x : ℝ) in 0..ε, g x) + ∫ (x : ℝ) in ε..Int.fract (t / T) * T + ⌊t / T⌋ • T, g x ≤
    sSup ((fun t ↦ ∫ (x : ℝ) in 0..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0..T, g x
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : NormedAddCommGroup E
F : Type u_4
G : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
op : E → F → G
hop : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry op)
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
C : ℝ
hC : ∀ (x : E) (y : F), ‖op x y‖ ≤ C * ‖x‖ * ‖y‖
⊢ ∫⁻ (z : α × β), ‖op (f z.1) (g z.2)‖ₑ ∂μ.prod ν ≤ ∫⁻ (z : α × β), ENNReal.ofReal C * ‖f z.1‖ₑ * ‖g z.2‖ₑ ∂μ.prod ν

Tactic:
gcongr with z

Goal state after:
case hfg
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : NormedAddCommGroup E
F : Type u_4
G : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
op : E → F → G
hop : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry op)
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
C : ℝ
hC : ∀ (x : E) (y : F), ‖op x y‖ ≤ C * ‖x‖ * ‖y‖
z : α × β
⊢ ‖op (f z.1) (g z.2)‖ₑ ≤ ENNReal.ofReal C * ‖f z.1‖ₑ * ‖g z.2‖ₑ
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
⊢ 0 ≤ 2 * π

Tactic:
positivity

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

Goal state before:
pp: c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → ∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1) = 0
⊢ HasSum (fun n ↦ ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)

Tactic:
have : (∮ z in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * π * I := by simp [hR.ne']

Goal state after:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → ∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1) = 0
this : ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹ = 2 * ↑π * I
⊢ HasSum (fun n ↦ ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: case inr
α : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
a b : ℝ
f : ℝ → α → E
h_int : Integrable (uncurry f) ((volume.restrict (uIoc a b)).prod μ)
hab : b ≤ a
⊢ ∫ (x : ℝ) in a..b, ∫ (y : α), f x y ∂μ = ∫ (y : α), ∫ (x : ℝ) in a..b, f x y ∂μ

Tactic:
· simp_rw [intervalIntegral.integral_of_ge hab]
    simp only [hab, Set.uIoc_of_ge] at h_int
    rw [integral_integral_swap h_int, integral_neg]

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

Goal state before:
pp: 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
ε' : ℝ
ε'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.real ↑J

Tactic:
positivity

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

Goal state before:
pp: F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ z ∈ sphere c R, ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
hq : iteratedDeriv n f c = n.factorial • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z
⊢ 0 < ↑n.factorial

Tactic:
positivity

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

Goal state before:
pp: case hf
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[≠] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
hc' : ContinuousOn (fun z ↦ (z - c)⁻¹) (sphere c r)
⊢ ContinuousOn f (sphere c r)

Tactic:
exact hc.mono <| subset_inter
          (sphere_subset_closedBall.trans <| closedBall_subset_closedBall hrR) hzne

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
⊢ (restrictProd p q) f = (restrictProd p q) g → f = g

Tactic:
hfg

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg : (restrictProd p q) f = (restrictProd p q) g
⊢ f = g
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case neg.inl
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
x : (p * q).SplittingField
hx : x ∈ ↑(p.aroots (p * q).SplittingField + q.aroots (p * q).SplittingField).toFinset
h : x ∈ p.aroots (p * q).SplittingField
this : Fact (map (algebraMap F (p * q).SplittingField) p).Splits
key :
  x = (algebraMap p.SplittingField (p * q).SplittingField) ↑((rootsEquivRoots p (p * q).SplittingField).invFun ⟨x, ⋯⟩)
⊢ f ((algebraMap p.SplittingField (p * q).SplittingField) ↑((rootsEquivRoots p (p * q).SplittingField).invFun ⟨x, ⋯⟩)) =
    g ((algebraMap p.SplittingField (p * q).SplittingField) ↑((rootsEquivRoots p (p * q).SplittingField).invFun ⟨x, ⋯⟩))

Tactic:
← AlgEquiv.restrictNormal_commutes,

Goal state after:
case neg.inl
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
x : (p * q).SplittingField
hx : x ∈ ↑(p.aroots (p * q).SplittingField + q.aroots (p * q).SplittingField).toFinset
h : x ∈ p.aroots (p * q).SplittingField
this : Fact (map (algebraMap F (p * q).SplittingField) p).Splits
key :
  x = (algebraMap p.SplittingField (p * q).SplittingField) ↑((rootsEquivRoots p (p * q).SplittingField).invFun ⟨x, ⋯⟩)
⊢ (algebraMap p.SplittingField (p * q).SplittingField)
      ((AlgEquiv.restrictNormal f p.SplittingField) ↑((rootsEquivRoots p (p * q).SplittingField).invFun ⟨x, ⋯⟩)) =
    g ((algebraMap p.SplittingField (p * q).SplittingField) ↑((rootsEquivRoots p (p * q).SplittingField).invFun ⟨x, ⋯⟩))
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
e : σ ≃ τ
h : ((rename ⇑e) φ).IsSymmetric
⊢ φ.IsSymmetric

Tactic:
by simpa using (IsSymmetric.rename (R := R) h e.symm)

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case neg.inr
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
x : (p * q).SplittingField
hx : x ∈ ↑(p.aroots (p * q).SplittingField + q.aroots (p * q).SplittingField).toFinset
h : x ∈ q.aroots (p * q).SplittingField
this : Fact (map (algebraMap F (p * q).SplittingField) q).Splits
key :
  x = (algebraMap q.SplittingField (p * q).SplittingField) ↑((rootsEquivRoots q (p * q).SplittingField).invFun ⟨x, ⋯⟩)
⊢ f ((algebraMap q.SplittingField (p * q).SplittingField) ↑((rootsEquivRoots q (p * q).SplittingField).invFun ⟨x, ⋯⟩)) =
    g ((algebraMap q.SplittingField (p * q).SplittingField) ↑((rootsEquivRoots q (p * q).SplittingField).invFun ⟨x, ⋯⟩))

Tactic:
← AlgEquiv.restrictNormal_commutes,

Goal state after:
case neg.inr
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
x : (p * q).SplittingField
hx : x ∈ ↑(p.aroots (p * q).SplittingField + q.aroots (p * q).SplittingField).toFinset
h : x ∈ q.aroots (p * q).SplittingField
this : Fact (map (algebraMap F (p * q).SplittingField) q).Splits
key :
  x = (algebraMap q.SplittingField (p * q).SplittingField) ↑((rootsEquivRoots q (p * q).SplittingField).invFun ⟨x, ⋯⟩)
⊢ (algebraMap q.SplittingField (p * q).SplittingField)
      ((AlgEquiv.restrictNormal f q.SplittingField) ↑((rootsEquivRoots q (p * q).SplittingField).invFun ⟨x, ⋯⟩)) =
    g ((algebraMap q.SplittingField (p * q).SplittingField) ↑((rootsEquivRoots q (p * q).SplittingField).invFun ⟨x, ⋯⟩))
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
⊢ (map (algebraMap F (p.comp q).SplittingField) p).Splits

Tactic:
by
  let P : F[X] → Prop := fun r => (r.map (algebraMap F (r.comp q).SplittingField)).Splits
  have key1 : ∀ {r : F[X]}, Irreducible r → P r := by
    intro r hr
    by_cases hr' : natDegree r = 0
    · exact Splits.of_natDegree_le_one <| natDegree_map_le.trans (hr'.trans_le zero_le_one)
    obtain ⟨x, hx⟩ :=
      Splits.exists_eval_eq_zero (SplittingField.splits (r.comp q)) fun h =>
        hr' ((mul_eq_zero.mp (natDegree_comp.symm.trans (natDegree_eq_of_degree_eq_some
          (by rwa [degree_map] at h)))).resolve_right hq)
    rw [eval_map_algebraMap, aeval_comp] at hx
    have h_normal : Normal F (r.comp q).SplittingField := SplittingField.instNormal (r.comp q)
    have qx_int := Normal.isIntegral h_normal (aeval x q)
    exact (h_normal.splits _).of_dvd (map_ne_zero (minpoly.ne_zero (h_normal.isIntegral _)))
      ((map_dvd_map' _).mpr ((minpoly.irreducible qx_int).dvd_symm hr (minpoly.dvd F _ hx)))
  have key2 : ∀ {p₁ p₂ : F[X]}, P p₁ → P p₂ → P (p₁ * p₂) := by
    intro p₁ p₂ hp₁ hp₂
    by_cases h₁ : p₁.comp q = 0
    · rcases comp_eq_zero_iff.mp h₁ with h | h
      · rw [h, zero_mul]
        simp [P]
      · exact False.elim (hq (by rw [h.2, natDegree_C]))
    by_cases h₂ : p₂.comp q = 0
    · rcases comp_eq_zero_iff.mp h₂ with h | h
      · simp [h, P]
      · exact False.elim (hq (by rw [h.2, natDegree_C]))
    have key := mul_splits_in_splittingField_of_mul h₁ h₂ hp₁ hp₂
    rwa [← mul_comp] at key
  exact
    WfDvdMonoid.induction_on_irreducible p (by simp) (fun _ hu => hu.splits.map _)
      fun _ _ _ h => key2 (key1 h)

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✝ : DecidableEq σ
⊢ (fun x ↦ x ∈ Set.univ) = fun x ↦ Nat.Partition.ofSym x = Nat.Partition.indiscrete 1

Tactic:
Set.mem_univ,

Goal state after:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
⊢ (fun x ↦ True) = fun x ↦ Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
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
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
t : Set ℂ
ht : t ∈ 𝓝 w
g : ℝ → ℂ := fun x ↦ w + ↑x
this✝ : Tendsto g (𝓝 0) (𝓝 w)
l u : ℝ
hlu₀ : 0 ∈ Ioo l u
hlu_sub : Ioo l u ⊆ g ⁻¹' (t ∩ ball c R)
hsub : Ioo l u ⊆ g ⁻¹' s
this : (Ioo l u).Countable
⊢ False

Tactic:
rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ioo_real (hlu₀.1.trans hlu₀.2)] at this

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
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
t : Set ℂ
ht : t ∈ 𝓝 w
g : ℝ → ℂ := fun x ↦ w + ↑x
this✝ : Tendsto g (𝓝 0) (𝓝 w)
l u : ℝ
hlu₀ : 0 ∈ Ioo l u
hlu_sub : Ioo l u ⊆ g ⁻¹' (t ∩ ball c R)
hsub : Ioo l u ⊆ g ⁻¹' s
this : Cardinal.continuum ≤ Cardinal.aleph0
⊢ False
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: case inr.inl
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 : (map f p).natDegree < i
⊢ 0 ≤ B ^ ((map f p).natDegree - i) * ↑((map f p).natDegree.choose i)

Tactic:
positivity

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

Goal state before:
pp: case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f [[a, b]]
Hd : ∀ x ∈ Set.Ioo (min a b) (max a b) \ s, HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
hab : b ≤ a
⊢ ∫ (x : ℝ) in a..b, f' x = f b - f a

Tactic:
· simp only [uIcc_of_ge hab, min_eq_right hab, max_eq_left hab] at *
    rw [intervalIntegral.integral_symm, neg_eq_iff_eq_neg, neg_sub]
    exact integral_eq_of_hasDerivAt_off_countable_of_le f f' hab hs Hc Hd Hi.symm

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: case refine_2
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))⌉₊
this :
  (⋃ f,
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), f.coeff i ∈ Icc (-↑C) ↑C),
        ↑(map (algebraMap ℤ K) f).roots.toFinset).Finite
x : K
hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖φ x‖ ≤ B}
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
i : ℕ
⊢ ↑|(minpoly ℤ x).coeff i| ≤ ↑↑C

Tactic:
refine (Eq.trans_le ?_ <| coeff_bdd_of_norm_le hx.2 i).trans (Nat.le_ceil _)

Goal state after:
case refine_2
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))⌉₊
this :
  (⋃ f,
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), f.coeff i ∈ Icc (-↑C) ↑C),
        ↑(map (algebraMap ℤ K) f).roots.toFinset).Finite
x : K
hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖φ x‖ ≤ B}
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
i : ℕ
⊢ ↑|(minpoly ℤ x).coeff i| = ‖(minpoly ℚ x).coeff i‖
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.IsNontrivial
a✝ : MulArchimedean (ofClass v).ValueGroup₀
f : Additive (ofClass v).ValueGroup₀ˣ →+o ℝ
hf : Injective ⇑f
e : (ofClass v).ValueGroup₀ˣ →* Multiplicative ℝ := AddMonoidHom.toMultiplicativeRight ↑f
he : StrictMono ⇑e
x : Multiplicative ℝ
⊢ 0 ≤ 2 ^ (↑x).log

Tactic:
positivity

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

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.IsNontrivial
a✝ : MulArchimedean (ofClass v).ValueGroup₀
f : Additive (ofClass v).ValueGroup₀ˣ →+o ℝ
hf : Injective ⇑f
e : (ofClass v).ValueGroup₀ˣ →* Multiplicative ℝ := AddMonoidHom.toMultiplicativeRight ↑f
he : StrictMono ⇑e
x : Multiplicative ℝ
⊢ ¬2 ^ (↑x).log = 0

Tactic:
positivity

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

Goal state before:
pp: case a
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 : ℝ
⊢ x ∈ upperBounds (ratLt' 0) → 0 ≤ x

Tactic:
rw [mem_upperBounds]

Goal state after:
case a
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 : ℝ
⊢ (∀ x_1 ∈ ratLt' 0, x_1 ≤ x) → 0 ≤ x
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r s : ℝ
this : ∀ (x y : X) (r s : ℝ), r ≤ s → ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)
hrs : s < r
⊢ ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)

Tactic:
rw [disjoint_comm, ← or_assoc, or_comm (b := (_ : Set X) ⊆ _), or_assoc]
    exact this y x s r hrs.le

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

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r s : ℝ
this :
  ∀ (x y : X) (r s : ℝ),
    r ≤ s →
      closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)
hrs : s < r
⊢ closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)

Tactic:
rw [disjoint_comm, ← or_assoc, or_comm (b := (_ : Set X) ⊆ _), or_assoc]
    exact this y x s r hrs.le

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
⊢ lexOrder 0 = ⊤

Tactic:
by
  unfold lexOrder
  rw [dif_pos rfl]

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: case inr
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x : L
hx : v x ≠ 0 ∧ v x ≠ 1
h : v x⁻¹ ≤ 1
⊢ ∃ x, 1 < ‖x‖

Tactic:
use x
      simp only [map_inv₀, inv_le_one₀ <| zero_lt_iff.mpr hx.1] at h
      simp only [toNormedField.one_lt_norm_iff, lt_of_le_of_ne h hx.2.symm]

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: case inr
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x : L
hx : v x ≠ 0 ∧ v x ≠ 1
h : v x⁻¹ ≤ 1
⊢ ∃ x, 1 < ‖x‖

Tactic:
· use x
      simp only [map_inv₀, inv_le_one₀ <| zero_lt_iff.mpr hx.1] at h
      simp only [toNormedField.one_lt_norm_iff, lt_of_le_of_ne h hx.2.symm]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
j : R
inst✝ : W.IsElliptic
hu : Fact (IsUnit 2)
⊢ IsUnit (ofJ1728 R).Δ

Tactic:
ofJ1728_Δ

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
j : R
inst✝ : W.IsElliptic
hu : Fact (IsUnit 2)
⊢ IsUnit (-64)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (IsUnit 2)
⊢ (-48) ^ 3 = (ofJ1728 R).Δ * 1728

Tactic:
ofJ1728_Δ

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (IsUnit 2)
⊢ (-48) ^ 3 = -64 * 1728
Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer

Goal state before:
pp: case snd
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
r : J.R
⊢ (ConcreteCategory.hom (I.multicospan.map (WalkingMulticospan.Hom.snd r)))
      ((fun i ↦
          match i with
          | WalkingMulticospan.left i => s.val i
          | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
        (WalkingMulticospan.left (J.snd r))) =
    (fun i ↦
        match i with
        | WalkingMulticospan.left i => s.val i
        | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
      (WalkingMulticospan.right r)

Tactic:
exact (s.property r).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hz : P z = Q z
hQz : Q z ∈ nonZeroDivisors R
⊢ P ≈ Q ↔ P = Q

Tactic:
refine ⟨?_, Quotient.exact.comp <| congrArg _⟩

Goal state after:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hz : P z = Q z
hQz : Q z ∈ nonZeroDivisors R
⊢ P ≈ Q → P = Q
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
h : ¬P ≈ Q
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ W'.add (u • P) (v • Q) = (u * v) ^ 2 • W'.add P Q

Tactic:
rw [add_of_not_equiv <| h.comp (smul_equiv_smul P Q hu hv).mp, addXYZ_smul, add_of_not_equiv h]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ (eval P) W'.polynomialY = 2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2

Tactic:
rw [polynomialY_eq]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ (eval P) (C 2 * Y * Z + C W'.a₁ * X * Z + C W'.a₃ * Z ^ 2) = 2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2