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

Goal state before:
pp: K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : Field A
inst✝¹ : Algebra ℚ A
inst✝ : IsAlgClosed A
x : K
⊢ (range fun φ ↦ φ x) = (minpoly ℚ x).rootSet A

Tactic:
by

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

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a b : ℝ × ℝ
hle : a ≤ b
Hcf : ContinuousOn f (Set.Icc a b)
Hcg : ContinuousOn g (Set.Icc a b)
Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume
⊢ ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ ∅, HasFDerivAt g (g' x) x

Tactic:
by

Goal state after:
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
z : ℂ
hz1 : (aeval z) p = 0
hz2 : z.im = 0
key : (IsScalarTower.toAlgHom ℚ ℝ ℂ) z.re = z
⊢ (IsScalarTower.toAlgHom ℚ ℝ ℂ) ((aeval z.re) p) = (IsScalarTower.toAlgHom ℚ ℝ ℂ) 0

Tactic:
by

Goal state after:
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 : ℕ
⊢ ‖(minpoly ℚ x).coeff i‖ ≤ max B 1 ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))

Tactic:
by

Goal state after:
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
⊢ ∀ (z : ℂ), z ∈ b ↔ (aeval z) p = 0 ∧ z.im = 0

Tactic:
by

Goal state after:
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 ℂ)), ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))) w = w ↔ (↑w).im = 0

Tactic:
by

Goal state after:
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 Γ₀
v : F →*₀ Γ₀
⊢ ∀ ⦃a : ↥(MonoidHom.mrange v)⦄, 0 < a → ∀ ⦃b c : ↥(MonoidHom.mrange v)⦄, b < c → a * b < a * c

Tactic:
by

Goal state after:
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 Γ₀
v : F →*₀ Γ₀
⊢ ⊥ ∈ MonoidHom.mrange v

Tactic:
by

Goal state after:
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 Γ₀
v : F →*₀ Γ₀
a : ↥(MonoidHom.mrange v)
⊢ ⟨⊥, ⋯⟩ ≤ a

Tactic:
by

Goal state after:
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 Γ₀
v : F →*₀ Γ₀
a : ↥(MonoidHom.mrange v)
⊢ 0 ≤ a

Tactic:
by

Goal state after:
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 Γ₀
hv : v.Integers O
⊢ WfDvdMonoid O ↔ WellFounded ((fun x1 x2 ↦ x1 > x2) on ⇑v ∘ ⇑(algebraMap O F))

Tactic:
by

Goal state after:
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
h : (Set.range (⇑v ∘ ⇑(algebraMap O F))).WellFoundedOn fun x1 x2 ↦ x1 > x2
⊢ ∀ a ∈ {x | x ≤ 1}, ∀ b ∈ {x | x ≤ 1}, a > b → ((fun x1 x2 ↦ x1 > x2) on Subtype.val) a b

Tactic:
by

Goal state after:
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 | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖φ x‖ ≤ B}.Finite

Tactic:
by

Goal state after:
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
h : (Set.range (⇑v ∘ ⇑(algebraMap O F))).WellFoundedOn fun x1 x2 ↦ x1 > x2
y : O
hx : v ((algebraMap O F) y) ≤ 1
⊢ v ((algebraMap O F) y) = v ((algebraMap O F) y)

Tactic:
by

Goal state after:
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
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ ≤ 1
a : ℕ
x✝ : a ∈ univ
φ : K →+* A
⊢ ‖φ ((fun x_1 ↦ x ^ x_1) a)‖ ≤ 1

Tactic:
by

Goal state after:
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
⊢ WellFounded ((fun x1 x2 ↦ x1 > x2) on ⇑v ∘ ⇑(algebraMap O F)) ↔
    Nonempty (↥(MonoidHom.mrange v) ≃*o WithZero (Multiplicative ℤ))

Tactic:
by

Goal state after:
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
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ ≤ 1
⊢ ∃ n, ∃ (_ : 0 < n), x ^ n = 1

Tactic:
by

Goal state after:
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✝ : MulArchimedean ↥(MonoidHom.mrange v)
hv : v.Integers O
⊢ IsPrincipalIdealRing O ↔ ¬DenselyOrdered ↑(Set.range ⇑v)

Tactic:
by

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
num : ℤ
n den : ℕ
hn : 0 < n
x : M
⊢ (num * ↑n) • 1 < (↑n * ↑den) • x ↔ num • 1 < den • x

Tactic:
by

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
⊢ (u.num * ↑v.den) • 1 < (↑u.den * ↑v.den) • x

Tactic:
by

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

Tactic:
by

Goal state after:
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
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ = 1
⊢ ∃ n, ∃ (_ : 0 < n), x ^ n = 1

Tactic:
by

Goal state after:
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 →+* ℂ
⊢ K →+* ℂ

Tactic:
by

Goal state after:
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 →+* ℂ
⊢ (lift K φ).comp (algebraMap k K) = φ

Tactic:
by

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
⊢ 0 < ↑(u + v).den

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
⊢ Function.Involutive conjugate

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
⊢ place (conjugate φ) = place φ

Tactic:
by

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
⊢ (u + v).num • 1 < (u + v).den • (x + y)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
k : Type u_2
inst✝ : Field k
φ : K →+* ℂ
hφ : IsReal φ
⊢ (φ 1).re = 1

Tactic:
by

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
num : ℤ
den : ℕ
x : M
h : num • 1 ≤ den • x
n : ℤ
hn : x ≤ n • 1
⊢ 0 < 1

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
k : Type u_2
inst✝ : Field k
φ : K →+* ℂ
hφ : IsReal φ
⊢ ∀ (x y : K), (φ (x * y)).re = (φ x).re * (φ y).re

Tactic:
by

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
num : ℤ
den : ℕ
x : M
h : num • 1 ≤ den • x
n : ℤ
hn : x ≤ n • 1
⊢ num ≤ n * ↑den

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
k : Type u_2
inst✝ : Field k
φ : K →+* ℂ
hφ : IsReal φ
⊢ (φ 0).re = 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
k : Type u_2
inst✝ : Field k
φ : K →+* ℂ
hφ : IsReal φ
⊢ ∀ (x y : K), (φ (x + y)).re = (φ x).re + (φ y).re

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
k : Type u_2
inst✝ : Field k
f : k →+* K
φ : K →+* ℂ
hφ : IsReal φ
⊢ IsReal (φ.comp f)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
k : Type u_2
inst✝ : Field k
f : k ≃+* K
φ : K →+* ℂ
H : IsReal (φ.comp ↑f)
⊢ IsReal φ

Tactic:
by

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

Goal state before:
pp: case h
K : Type u_1
inst✝³ : Field K
k : Type u_2
inst✝² : Field k
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
φ ψ : K →+* ℂ
h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)
this✝¹ : Algebra k ℂ := (φ.comp (algebraMap k K)).toAlgebra
this✝ : Algebra K ℂ := φ.toAlgebra
this : IsScalarTower k K ℂ
ψ' : K →ₐ[k] ℂ := { toRingHom := ψ, commutes' := ⋯ }
x : K
⊢ (φ.comp ↑(ψ'.restrictNormal' K).symm.symm) x = ψ x

Tactic:
exact AlgHom.restrictNormal_commutes ψ' K x

Goal state after:
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✝ : IsGalois k K
φ ψ : K →+* ℂ
h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)
⊢ ∃ σ, φ.comp ↑σ.symm = ψ

Tactic:
by

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
num : ℤ
den : ℕ
hden : den ≠ 0
x : M
⊢ mkRat num den ∈ ratLt x ↔ num • 1 < den • x

Tactic:
by

Goal state after:
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
φ : K →+* ℂ
σ : Gal(K/k)
h : IsConj φ σ
⊢ IsReal (φ.comp (algebraMap k K))

Tactic:
by

Goal state after:
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
φ : K →+* ℂ
σ : Gal(K/k)
hσ : IsConj φ σ
x : K
⊢ (conjugate φ) x = (φ.comp ↑σ.symm) x

Tactic:
by

Goal state after:
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
φ : K →+* ℂ
σ : Gal(K/k)
hσ : IsConj φ σ
x : K
⊢ σ (σ x) = x

Tactic:
by

Goal state after:
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
φ : K →+* ℂ
σ : Gal(K/k)
hσ : IsConj φ σ
ν : Gal(K/k)
⊢ IsConj (φ.comp ↑ν) (ν⁻¹ * σ * ν)

Tactic:
by

Goal state after:
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
hc0 :
  ∀ (w : ↑(p.rootSet ℂ)), ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))) w = w ↔ (↑w).im = 0
⊢ ∀ (z : ℂ), z ∈ c ↔ (aeval z) p = 0 ∧ z.im ≠ 0

Tactic:
by

Goal state after:
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
φ : K →+* ℂ
σ : Gal(K/k)
hσ : IsConj φ σ
hσ' : σ ≠ 1
⊢ σ ^ 2 = 1

Tactic:
by

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

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
ψ : K →+* ℂ
inst✝ : Algebra K L
φ : ComplexEmbedding.Extension L ψ
h : ¬IsReal ψ
⊢ (conjugate ↑φ).comp (algebraMap K L) ≠ ψ

Tactic:
by

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

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
φ : L →+* ℂ
h : IsUnmixed K φ
⊢ IsReal (φ.comp (algebraMap K L)) ↔ IsReal φ

Tactic:
by

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
x : M
n : ℕ
hn : x ≤ n • 1
num : ℤ
den : ℕ
den_nz✝ : den ≠ 0
reduced✝ : num.natAbs.Coprime den
this : num • 1 < den • x → num ≤ ↑n * ↑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:
by

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

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
ψ : K →+* ℂ
inst✝ : Algebra K L
⊢ Disjoint (unmixedEmbeddingsOver L ψ) (mixedEmbeddingsOver L ψ)

Tactic:
by

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

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
ψ : K →+* ℂ
inst✝ : Algebra K L
⊢ unmixedEmbeddingsOver L ψ ∪ mixedEmbeddingsOver L ψ = {φ | ComplexEmbedding.LiesOver φ ψ}

Tactic:
by

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
x : M
n : ℕ
hn : x ≤ n • 1
num : ℤ
den : ℕ
den_nz✝ : den ≠ 0
reduced✝ : num.natAbs.Coprime den
h : num • 1 < den • x
⊢ x ≤ ↑n • 1

Tactic:
by

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
x : M
⊢ BddAbove (ratLt x)

Tactic:
by

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
x : M
hneg : x < 0
n : ℕ
hn : -x - x ≤ n • 1
this : -(n • 1) < x
⊢ Rat.ofInt (-↑n) ∈ ratLt x

Tactic:
by

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
x : M
hneg : x < 0
n : ℕ
hn : -x - x ≤ n • 1
⊢ -x < -x - x

Tactic:
by

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
⊢ Rat.ofInt (-1) ∈ ratLt 0

Tactic:
by

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
x : M
hxpos : 0 < x
n : ℕ
hn : 1 ≤ n • x
⊢ n + 1 ≠ 0

Tactic:
by

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
x : M
hxpos : 0 < x
n : ℕ
hn : 1 ≤ n • x
⊢ (Int.natAbs 1).Coprime (n + 1)

Tactic:
by

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
x : M
hxpos : 0 < x
n : ℕ
hn : 1 ≤ n • x
⊢ n < n + 1

Tactic:
by

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
x : M
⊢ (ratLt x).Nonempty

Tactic:
by

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
x y : M
a : ℚ
h : a.num • 1 < a.den • (x + y)
k : ℕ
hk : 1 + 1 ≤ k • (a.den • (x + y) - a.num • 1)
⊢ k ≠ 0

Tactic:
by

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
⊢ StrictMono ⇑e

Tactic:
by

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 ℝ
⊢ 0 ≤ 2 ^ (↑x).log

Tactic:
by

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 ℝ
⊢ NNReal.mk (2 ^ (↑x).log) ⋯ ≠ 0

Tactic:
by

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
⊢ Units.mk0 (NNReal.mk (2 ^ (↑1).log) ⋯) ⋯ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: p : ℚ[X]
⊢ (p.rootSet ℂ).toFinset.card =
    (p.rootSet ℝ).toFinset.card + ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card

Tactic:
by

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✝¹ x✝ : Multiplicative ℝ
⊢ Units.mk0 (NNReal.mk (2 ^ (↑(x✝¹ * x✝)).log) ⋯) ⋯ =
    Units.mk0 (NNReal.mk (2 ^ (↑x✝¹).log) ⋯) ⋯ * Units.mk0 (NNReal.mk (2 ^ (↑x✝).log) ⋯) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
⊢ Fintype.card ↑(p.rootSet ℂ) = p.natDegree

Tactic:
by

Goal state after: