mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
z : A
hz : z ∈ (map (algebraMap ℚ A) (minpoly ℚ x)).roots.toFinset
⊢ ‖z‖ ≤ B

Tactic:
]

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
z : A
hz : z ∈ (map (algebraMap ℚ A) (minpoly ℚ x)).roots.toFinset
⊢ ‖z‖ ≤ B
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: case refine_1
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)
⊢ (minpoly ℚ x).natDegree ≤ finrank ℚ K

Tactic:
]

Goal state after:
case refine_1
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)
⊢ (minpoly ℚ x).natDegree ≤ finrank ℚ K
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun a ↦ ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ (aeval z) p = 0 ∧ z.im = 0
w : ↑(p.rootSet ℂ)
⊢ (AlgEquiv.restrictScalars ℚ conjAe) ↑w = ↑w ↔ (↑w).im = 0

Tactic:
]

Goal state after:
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun a ↦ ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ (aeval z) p = 0 ∧ z.im = 0
w : ↑(p.rootSet ℂ)
⊢ (AlgEquiv.restrictScalars ℚ conjAe) ↑w = ↑w ↔ (↑w).im = 0
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:
← @Int.cast_le ℝ

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| ≤ ↑↑C
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:
]

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| ≤ ↑↑C
Module: Mathlib.RingTheory.Valuation.Archimedean

Goal state before:
pp: F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
⊢ ((Set.range (⇑v ∘ ⇑(algebraMap O F))).WellFoundedOn fun x1 x2 ↦ x1 > x2) ↔
    {x | x ≤ 1}.WellFoundedOn fun x1 x2 ↦ x1 > x2

Tactic:
]

Goal state after:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
⊢ ((Set.range (⇑v ∘ ⇑(algebraMap O F))).WellFoundedOn fun x1 x2 ↦ x1 > x2) ↔
    {x | x ≤ 1}.WellFoundedOn fun x1 x2 ↦ x1 > x2
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case inr
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a₁ a₂ b₁ b₂ : ℝ
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) volume
this :
  ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
    ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
      (∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt f (f' x) x) →
        (∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt g (g' x) x) →
          IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) volume →
            b₁ ≤ a₁ →
              ∫ (x : ℝ) in b₁..a₁, ∫ (y : ℝ) in a₂..b₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) =
                (((∫ (x : ℝ) in b₁..a₁, g (x, b₂)) - ∫ (x : ℝ) in b₁..a₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (a₁, y)) -
                  ∫ (y : ℝ) in a₂..b₂, f (b₁, y)
h₁ : ¬a₁ ≤ b₁
⊢ ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) =
    (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (b₁, y)) -
      ∫ (y : ℝ) in a₂..b₂, f (a₁, y)

Tactic:
]

Goal state after:
case inr
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a₁ a₂ b₁ b₂ : ℝ
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) volume
this :
  ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
    ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
      (∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt f (f' x) x) →
        (∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt g (g' x) x) →
          IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) volume →
            b₁ ≤ a₁ →
              ∫ (x : ℝ) in b₁..a₁, ∫ (y : ℝ) in a₂..b₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) =
                (((∫ (x : ℝ) in b₁..a₁, g (x, b₂)) - ∫ (x : ℝ) in b₁..a₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (a₁, y)) -
                  ∫ (y : ℝ) in a₂..b₂, f (b₁, y)
h₁ : ¬a₁ ≤ b₁
⊢ ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) =
    (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (b₁, y)) -
      ∫ (y : ℝ) in a₂..b₂, f (a₁, y)
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)| = |↑((minpoly ℤ x).coeff i)|

Tactic:
]

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

Goal state before:
pp: K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ ≤ 1
a b : ℕ
habne : a ≠ b
h : x ^ (a - b) = 1 ∨ x ^ b = 0
hlt : b < a
⊢ x ^ (a - b) = 1

Tactic:
]

Goal state after:
K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ ≤ 1
a b : ℕ
habne : a ≠ b
h : x ^ (a - b) = 1 ∨ x ^ b = 0
hlt : b < a
⊢ x ^ (a - b) = 1
Module: Mathlib.RingTheory.Valuation.Archimedean

Goal state before:
pp: case inr
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
h✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
this✝¹ : IsDomain O
this✝ : ValuationRing O
this : IsPrincipalIdealRing O ↔ WfDvdMonoid O
⊢ ¬DenselyOrdered ↥(MonoidHom.mrange v)

Tactic:
]

Goal state after:
case inr
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
h✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
this✝¹ : IsDomain O
this✝ : ValuationRing O
this : IsPrincipalIdealRing O ↔ WfDvdMonoid O
⊢ ¬DenselyOrdered ↥(MonoidHom.mrange v)
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
num : ℤ
n den : ℕ
hn : 0 < n
x : M
⊢ ↑n • num • 1 < ↑n • den • x ↔ num • 1 < den • x

Tactic:
]

Goal state after:
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : One M
num : ℤ
n den : ℕ
hn : 0 < n
x : M
⊢ ↑n • num • 1 < ↑n • den • x ↔ num • 1 < den • x
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
u v : ℚ
x y : M
hu : u.num • 1 < u.den • x
hv : v.num • 1 < v.den • y
hu' : (u.num * ↑v.den) • 1 < (↑u.den * ↑v.den) • x
this : ((u + v).num * ↑u.den * ↑v.den) • 1 < ↑(u + v).den • (↑u.den * ↑v.den) • (x + y)
⊢ ((u + v).num * ↑u.den * ↑v.den) • 1 < ↑(u + v).den • (↑u.den * ↑v.den) • (x + y)

Tactic:
]

Goal state after:
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : One M
u v : ℚ
x y : M
hu : u.num • 1 < u.den • x
hv : v.num • 1 < v.den • y
hu' : (u.num * ↑v.den) • 1 < (↑u.den * ↑v.den) • x
this : ((u + v).num * ↑u.den * ↑v.den) • 1 < ↑(u + v).den • (↑u.den * ↑v.den) • (x + y)
⊢ ((u + v).num * ↑u.den * ↑v.den) • 1 < ↑(u + v).den • (↑u.den * ↑v.den) • (x + y)
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
u v : ℚ
x y : M
hu : u.num • 1 < u.den • x
hv : v.num • 1 < v.den • y
hu' : (u.num * ↑v.den) • 1 < (↑u.den * ↑v.den) • x
⊢ ↑(u + v).den • (u.num * ↑v.den + v.num * ↑u.den) • 1 < ↑(u + v).den • (↑u.den * ↑v.den) • (x + y)

Tactic:
]

Goal state after:
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : One M
u v : ℚ
x y : M
hu : u.num • 1 < u.den • x
hv : v.num • 1 < v.den • y
hu' : (u.num * ↑v.den) • 1 < (↑u.den * ↑v.den) • x
⊢ ↑(u + v).den • (u.num * ↑v.den + v.num * ↑u.den) • 1 < ↑(u + v).den • (↑u.den * ↑v.den) • (x + y)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
k : Type u_2
inst✝² : Field k
inst✝¹ : Algebra k K
inst✝ : Algebra.IsAlgebraic k K
φ : k →+* ℂ
this : Algebra k ℂ := φ.toAlgebra
⊢ φ = φ

Tactic:
]

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
u v : ℚ
x y : M
hu : u.num • 1 < u.den • x
hv : v.num • 1 < v.den • y
hu' : (u.num * ↑v.den) • 1 < (↑u.den * ↑v.den) • x
⊢ (u.num * ↑v.den + v.num * ↑u.den) • 1 < (↑u.den * ↑v.den) • (x + y)

Tactic:
]

Goal state after:
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : One M
u v : ℚ
x y : M
hu : u.num • 1 < u.den • x
hv : v.num • 1 < v.den • y
hu' : (u.num * ↑v.den) • 1 < (↑u.den * ↑v.den) • x
⊢ (u.num * ↑v.den + v.num * ↑u.den) • 1 < (↑u.den * ↑v.den) • (x + y)
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
u v : ℚ
x y : M
hu : u.num • 1 < u.den • x
hv : v.num • 1 < v.den • y
hu' : (u.num * ↑v.den) • 1 < (↑u.den * ↑v.den) • x
⊢ (u.num * ↑v.den) • 1 + (v.num * ↑u.den) • 1 < (↑u.den * ↑v.den) • x + (↑u.den * ↑v.den) • y

Tactic:
]

Goal state after:
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : One M
u v : ℚ
x y : M
hu : u.num • 1 < u.den • x
hv : v.num • 1 < v.den • y
hu' : (u.num * ↑v.den) • 1 < (↑u.den * ↑v.den) • x
⊢ (u.num * ↑v.den) • 1 + (v.num * ↑u.den) • 1 < (↑u.den * ↑v.den) • x + (↑u.den * ↑v.den) • y
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
num : ℤ
den : ℕ
x : M
h : num • 1 ≤ den • x
n : ℤ
hn : x ≤ n • 1
⊢ den • x ≤ ↑den • n • 1

Tactic:
]

Goal state after:
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : LinearOrder M
inst✝³ : IsOrderedAddMonoid M
inst✝² : One M
inst✝¹ : ZeroLEOneClass M
inst✝ : NeZero 1
num : ℤ
den : ℕ
x : M
h : num • 1 ≤ den • x
n : ℤ
hn : x ≤ n • 1
⊢ den • x ≤ ↑den • n • 1
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
num : ℤ
den : ℕ
hden : den ≠ 0
x : M
⊢ (mkRat num den).num • 1 < (mkRat num den).den • x ↔ num • 1 < den • x

Tactic:
]

Goal state after:
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : One M
num : ℤ
den : ℕ
hden : den ≠ 0
x : M
⊢ (mkRat num den).num • 1 < (mkRat num den).den • x ↔ num • 1 < den • x
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: case a
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ (starRingEnd ℂ) (φ x) = φ x

Tactic:
]

Goal state after:
case a
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ (starRingEnd ℂ) (φ x) = φ x
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: case a
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ (↑(hφ.embedding x)).im = (φ x).im

Tactic:
rw [ofReal_im, eq_comm, ← Complex.conj_eq_iff_im]
    exact RingHom.congr_fun hφ x

Goal state after:
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
⊢ ∀ x_1 ∈ {r | r.num • 1 < r.den • x}, x_1 ≤ ↑n

Tactic:
]

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
⊢ ∀ x_1 ∈ {r | r.num • 1 < r.den • x}, x_1 ≤ ↑n
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✝ }.num * ↑(↑n).den ≤
      (↑n).num * ↑{ num := num, den := den, den_nz := den_nz✝, reduced := reduced✝ }.den

Tactic:
]

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.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case neg.refine_2.refine_2.refine_2
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun a ↦ ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ (aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(p.rootSet ℂ)), ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))) w = w ↔ (↑w).im = 0
hc : ∀ (z : ℂ), z ∈ c ↔ (aeval z) p = 0 ∧ z.im ≠ 0
⊢ a.card = (b ∪ c).card

pp: case neg.refine_2.refine_2.refine_2
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun a ↦ ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ (aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(p.rootSet ℂ)), ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))) w = w ↔ (↑w).im = 0
hc : ∀ (z : ℂ), z ∈ c ↔ (aeval z) p = 0 ∧ z.im ≠ 0
⊢ Disjoint b c

Tactic:
]

Goal state after:
case neg.refine_2.refine_2.refine_2
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun a ↦ ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ (aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(p.rootSet ℂ)), ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))) w = w ↔ (↑w).im = 0
hc : ∀ (z : ℂ), z ∈ c ↔ (aeval z) p = 0 ∧ z.im ≠ 0
⊢ a.card = (b ∪ c).card

case neg.refine_2.refine_2.refine_2
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun a ↦ ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ (aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(p.rootSet ℂ)), ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))) w = w ↔ (↑w).im = 0
hc : ∀ (z : ℂ), z ∈ c ↔ (aeval z) p = 0 ∧ z.im ≠ 0
⊢ Disjoint b c
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
x y : M
a : ℚ
⊢ a ∈ ratLt (x + y) ↔ ∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a

Tactic:
]

Goal state after:
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 : ℚ
⊢ a ∈ ratLt (x + y) ↔ ∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a
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:
]

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)
⊢ ∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a