awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
inst_3 : IsGalois k K
φ ψ : K →+* ℂ
h : Eq (α := k →+* ℂ) (φ.comp (algebraMap k K)) (ψ.comp (algebraMap k K))
this_1 : Algebra k ℂ := RingHom.toAlgebra (φ.comp (algebraMap k K))
this_2 : Algebra K ℂ := φ.toAlgebra
this : IsScalarTower k K ℂ
ψ' : K →ₐ[k] ℂ := { toRingHom := ψ, commutes' := ⋯ }
h₁ : φ.comp (↑(AlgEquiv.symm (AlgEquiv.symm (ψ'.restrictNormal' K))) : K →+* K) = ψ
⊢ ∃ (σ : Gal(K/k)), φ.comp (↑σ.symm : K →+* K) = ψ

Tactic:
use (AlgHom.restrictNormal' ψ' K).symm

Premises used: AlgEquiv.symm, AlgHom.restrictNormal'
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
inst_3 : IsGalois k K
φ ψ : K →+* ℂ
h : Eq (α := k →+* ℂ) (φ.comp (algebraMap k K)) (ψ.comp (algebraMap k K))
this_1 : Algebra k ℂ := RingHom.toAlgebra (φ.comp (algebraMap k K))
this_2 : Algebra K ℂ := φ.toAlgebra
this : IsScalarTower k K ℂ
ψ' : K →ₐ[k] ℂ := { toRingHom := ψ, commutes' := ⋯ }
h₁ :
  ∀ (x : K),
    Eq (α := ℂ) ((φ.comp (↑(AlgEquiv.symm (AlgEquiv.symm (ψ'.restrictNormal' K))) : K →+* K) : (a : K) → ℂ) x : ℂ)
      ((ψ : (a : K) → ℂ) x : ℂ)
⊢ φ.comp (↑(AlgEquiv.symm (AlgEquiv.symm (ψ'.restrictNormal' K))) : K →+* K) = ψ

Tactic:
ext1 x
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
inst_3 : IsGalois k K
φ ψ : K →+* ℂ
h : Eq (α := k →+* ℂ) (φ.comp (algebraMap k K)) (ψ.comp (algebraMap k K))
this_1 : Algebra k ℂ := RingHom.toAlgebra (φ.comp (algebraMap k K))
this_2 : Algebra K ℂ := φ.toAlgebra
this : IsScalarTower k K ℂ
ψ' : K →ₐ[k] ℂ := { toRingHom := ψ, commutes' := ⋯ }
x : K
⊢ Eq (α := ℂ) ((φ.comp (↑(AlgEquiv.symm (AlgEquiv.symm (ψ'.restrictNormal' K))) : K →+* K) : (a : K) → ℂ) x : ℂ)
    ((ψ : (a : K) → ℂ) x : ℂ)

Tactic:
AlgHom.restrictNormal_commutes ψ' K x

Premises used: Classical.choose, AlgHom.restrictNormal_commutes
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
inst_3 : IsGalois k K
φ ψ : K →+* ℂ
h : Eq (α := k →+* ℂ) (φ.comp (algebraMap k K)) (ψ.comp (algebraMap k K))
this_1 : Algebra k ℂ := RingHom.toAlgebra (φ.comp (algebraMap k K))
this_2 : Algebra K ℂ := φ.toAlgebra
this : IsScalarTower k K ℂ
ψ' : K →ₐ[k] ℂ := { toRingHom := ψ, commutes' := ⋯ }
x : K
⊢ Eq (α := ℂ) ((φ.comp (↑(AlgEquiv.symm (AlgEquiv.symm (ψ'.restrictNormal' K))) : K →+* K) : (a : K) → ℂ) x : ℂ)
    ((ψ : (a : K) → ℂ) x : ℂ)

Tactic:
exact AlgHom.restrictNormal_commutes ψ' K x

Premises used: AlgHom.restrictNormal_commutes
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
h : IsConj φ σ
x : K
⊢ Eq (α := ℂ) ((φ : (a : K) → ℂ) ((σ : (a : K) → K) x : K) : ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ)

Tactic:
RingHom.congr_fun h.symm x

Premises used: RingHom.congr_fun, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
φ : K →+* ℂ
σ₁ σ₂ : Gal(K/k)
h₁ : IsConj φ σ₁
h₂ : IsConj φ σ₂
⊢ σ₁ = σ₂

Tactic:
AlgEquiv.ext fun x ↦ φ.injective ((h₁.eq x).trans (h₂.eq x).symm)

Premises used: NumberField.ComplexEmbedding.IsConj.eq, RingHom.injective, AlgEquiv.ext, Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
φ : K →+* ℂ
σ₁ σ₂ : Gal(K/k)
h₁ : IsConj φ σ₁
⊢ σ₁ = σ₂ ↔ IsConj φ σ₂

Tactic:
⟨fun e ↦ e ▸ h₁, h₁.ext⟩

Premises used: Eq.rec, NumberField.ComplexEmbedding.IsConj.ext, Iff.intro
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
h : IsConj φ σ
a :
  ∀ (x : k),
    Eq (α := ℂ) ((star (φ.comp (algebraMap k K)) : (a : k) → ℂ) x : ℂ) ((φ.comp (algebraMap k K) : (a : k) → ℂ) x : ℂ)
⊢ IsReal (φ.comp (algebraMap k K))

Tactic:
ext1 x
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
h : IsConj φ σ
x : k
⊢ Eq (α := ℂ) ((star (φ.comp (algebraMap k K)) : (a : k) → ℂ) x : ℂ) ((φ.comp (algebraMap k K) : (a : k) → ℂ) x : ℂ)

Tactic:
simp only [conjugate_coe_eq, RingHom.coe_comp, Function.comp_apply, ← h.eq,
    starRingEnd_apply, AlgEquiv.commutes]

Premises used: NumberField.ComplexEmbedding.IsConj.eq, AlgEquiv.commutes, starRingEnd_apply, RingHom.coe_comp, Function.comp_apply, NumberField.ComplexEmbedding.conjugate_coe_eq
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
φ : K →+* ℂ
⊢ IsConj.{u_1, u_2} (k := k) φ 1 ↔ IsReal φ

Tactic:
Iff.rfl

Premises used: IsSelfAdjoint, NumberField.ComplexEmbedding.IsConj, Iff.rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
hσ : IsConj φ σ
⊢ σ ≠ 1 ↔ ¬IsReal φ

Tactic:
not_iff_not.mpr ⟨fun h ↦ isConj_one_iff.mp (h ▸ hσ),
    fun h ↦ (IsConj.ext_iff hσ).mpr h.isConjGal_one⟩

Premises used: not_iff_not, Iff.mpr, Iff.intro, NumberField.ComplexEmbedding.IsConj.ext_iff, Iff.mp, NumberField.ComplexEmbedding.IsReal.isConjGal_one, NumberField.ComplexEmbedding.isConj_one_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
hσ : IsConj φ σ
x : K
⊢ Eq (α := ℂ) ((conjugate φ : (a : K) → ℂ) x : ℂ) ((φ.comp (↑σ.symm : K →+* K) : (a : K) → ℂ) x : ℂ)

Tactic:
simpa using congr_arg star (hσ.eq (σ.symm x))

Premises used: AlgEquiv.symm, NumberField.ComplexEmbedding.IsConj.eq, congr_arg, DFunLike.coe, Star.star
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
⊢ IsConj φ σ.symm ↔ IsConj φ σ

Tactic:
⟨IsConj.symm, IsConj.symm⟩

Premises used: NumberField.ComplexEmbedding.IsConj.symm, Iff.intro
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
hσ : IsConj φ σ
x : K
⊢ (σ : (a : K) → K) ((σ : (a : K) → K) x : K) = x

Tactic:
simp [← φ.injective.eq_iff, hσ.eq]

Premises used: NumberField.ComplexEmbedding.IsConj.eq, Function.Injective.eq_iff, RingHom.injective
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
hσ : IsConj φ σ
ν : Gal(K/k)
a :
  ∀ (x : K),
    Eq (α := ℂ) ((conjugate (φ.comp (↑ν : K →+* K)) : (a : K) → ℂ) x : ℂ)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (φ.comp (↑ν : K →+* K)) (↑(ν⁻¹ * σ * ν) : K →+* K) :
            (a : K) → ℂ)
          x :
        ℂ)
⊢ IsConj (φ.comp (↑ν : K →+* K)) (ν⁻¹ * σ * ν)

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
hσ : IsConj φ σ
ν : Gal(K/k)
x : K
⊢ Eq (α := ℂ) ((conjugate (φ.comp (↑ν : K →+* K)) : (a : K) → ℂ) x : ℂ)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (φ.comp (↑ν : K →+* K)) (↑(ν⁻¹ * σ * ν) : K →+* K) :
          (a : K) → ℂ)
        x :
      ℂ)

Tactic:
simpa [← AlgEquiv.mul_apply, ← mul_assoc] using RingHom.congr_fun hσ _

Premises used: RingHom.congr_fun, mul_assoc, AlgEquiv.mul_apply
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
hσ : IsConj φ σ
hσ' : σ ≠ 1
h : ∀ (a : K), Eq (α := K) ((HPow.hPow (β := ℕ) σ 2 : (a : K) → K) a : K) ((1 : (a : K) → K) a : K)
⊢ HPow.hPow (β := ℕ) σ 2 = 1

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
hσ : IsConj φ σ
hσ' : σ ≠ 1
a : K
⊢ Eq (α := K) ((HPow.hPow (β := ℕ) σ 2 : (a : K) → K) a : K) ((1 : (a : K) → K) a : K)

Tactic:
simpa using isConj_apply_apply hσ _

Premises used: NumberField.ComplexEmbedding.isConj_apply_apply
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
φ : L →+* ℂ
ψ : K →+* ℂ
inst_3 : ComplexEmbedding.LiesOver φ ψ
x : K
⊢ Eq (α := ℂ) ((φ : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ) ((ψ : (a : K) → ℂ) x : ℂ)

Tactic:
RingHom.ext_iff.1 (LiesOver.over φ ψ) _

Premises used: RingHom.ext_iff, Iff.mp, NumberField.ComplexEmbedding.LiesOver.over
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
φ : L →+* ℂ
ψ : K →+* ℂ
⊢ ComplexEmbedding.LiesOver φ ψ ↔ φ.comp (algebraMap K L) = ψ

Tactic:
⟨fun _ ↦ LiesOver.over φ ψ, fun h ↦ ⟨h⟩⟩

Premises used: Iff.intro, NumberField.ComplexEmbedding.LiesOver.mk, NumberField.ComplexEmbedding.LiesOver.over
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
ψ : K →+* ℂ
inst_2 : Algebra K L
φ : ComplexEmbedding.Extension L ψ
⊢ (↑φ : L →+* ℂ).comp (algebraMap K L) = ψ

Tactic:
φ.2.over

Premises used: NumberField.ComplexEmbedding.LiesOver.over
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
ψ : K →+* ℂ
inst_2 : Algebra K L
φ : ComplexEmbedding.Extension L ψ
h : ¬IsReal ψ
⊢ (conjugate (↑φ : L →+* ℂ)).comp (algebraMap K L) ≠ ψ

Tactic:
simp_all [ComplexEmbedding.isReal_iff, comp_eq]

Premises used: NumberField.ComplexEmbedding.Extension.comp_eq, NumberField.ComplexEmbedding.isReal_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
ψ : K →+* ℂ
inst_2 : Algebra K L
φ : ComplexEmbedding.Extension L ψ
h : ¬IsReal ψ
⊢ ¬IsReal (↑φ : L →+* ℂ)

Tactic:
mt (IsReal.comp _) (comp_eq φ ▸ h)

Premises used: mt, NumberField.ComplexEmbedding.IsReal.comp
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
φ : L →+* ℂ
h : IsUnmixed K φ
⊢ IsReal (φ.comp (algebraMap K L)) ↔ IsReal φ

Tactic:
aesop (add simp [IsReal.comp])

Premises used: NumberField.ComplexEmbedding.IsReal.comp
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
ψ : K →+* ℂ
inst_2 : Algebra K L
⊢ Disjoint (α := Set (L →+* ℂ)) (unmixedEmbeddingsOver L ψ) (mixedEmbeddingsOver L ψ)

Tactic:
grind [mixedEmbeddingsOver, unmixedEmbeddingsOver]

Premises used: NumberField.ComplexEmbedding.mixedEmbeddingsOver, NumberField.ComplexEmbedding.unmixedEmbeddingsOver
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
ψ : K →+* ℂ
inst_2 : Algebra K L
⊢ Eq (α := Set (L →+* ℂ)) (unmixedEmbeddingsOver L ψ ∪ mixedEmbeddingsOver L ψ)
    {φ : L →+* ℂ | ComplexEmbedding.LiesOver φ ψ}

Tactic:
grind [unmixedEmbeddingsOver, mixedEmbeddingsOver, ← Set.setOf_or]

Premises used: NumberField.ComplexEmbedding.mixedEmbeddingsOver, Set.setOf_or, NumberField.ComplexEmbedding.unmixedEmbeddingsOver
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
F : Type u_3
inst_2 : Field F
w : InfinitePlace K
f : k →+* K
a :
  ∀ (x : k),
    Eq (α := ℝ) ((place (w.embedding.comp f) : (a : k) → ℝ) x : ℝ)
      (((↑w : AbsoluteValue K ℝ).comp (f := f) ⋯ : (a : k) → ℝ) x : ℝ)
⊢ place (w.embedding.comp f) = (↑w : AbsoluteValue K ℝ).comp (f := f) ⋯

Tactic:
ext x
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
F : Type u_3
inst_2 : Field F
w : InfinitePlace K
f : k →+* K
x : k
a :
  Eq (α := ℝ) ((place (w.embedding.comp f) : (a : k) → ℝ) x : ℝ)
    (((↑w : AbsoluteValue K ℝ) : (a : K) → ℝ) ((f : (a : k) → K) x : K) : ℝ)
⊢ Eq (α := ℝ) ((place (w.embedding.comp f) : (a : k) → ℝ) x : ℝ)
    (((↑w : AbsoluteValue K ℝ).comp (f := f) ⋯ : (a : k) → ℝ) x : ℝ)

Tactic:
change _ = w.1 (f x)

Premises used: Subtype.val, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
F : Type u_3
inst_2 : Field F
w : InfinitePlace K
f : k →+* K
x : k
a :
  Eq (α := ℝ) ((place (w.embedding.comp f) : (a : k) → ℝ) x : ℝ)
    ((place (⋯.choose (p := fun (φ : K →+* ℂ) ↦ place φ = (↑w : AbsoluteValue K ℝ))) : (a : K) → ℝ)
        ((f : (a : k) → K) x : K) :
      ℝ)
⊢ Eq (α := ℝ) ((place (w.embedding.comp f) : (a : k) → ℝ) x : ℝ)
    (((↑w : AbsoluteValue K ℝ) : (a : K) → ℝ) ((f : (a : k) → K) x : K) : ℝ)

Tactic:
rw [← w.2.choose_spec]

Premises used: Exists.choose_spec, Subtype.property
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
F : Type u_3
inst_2 : Field F
w : InfinitePlace K
f : k →+* K
x : k
⊢ Eq (α := ℝ) ((place (w.embedding.comp f) : (a : k) → ℝ) x : ℝ)
    ((place (⋯.choose (p := fun (φ : K →+* ℂ) ↦ place φ = (↑w : AbsoluteValue K ℝ))) : (a : K) → ℝ)
        ((f : (a : k) → K) x : K) :
      ℝ)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
F : Type u_3
inst_2 : Field F
w : InfinitePlace K
f : k →+* K
a a₁ :
  ∀ (x : k),
    Eq (α := ℝ) ((place (w.embedding.comp f) : (a : k) → ℝ) x : ℝ)
      (((↑w : AbsoluteValue K ℝ).comp (f := f) ⋯ : (a : k) → ℝ) x : ℝ)
a₂ a₃ :
  ∀ (x : k),
    Eq (α := ℝ) ((place (w.embedding.comp f) : (a : k) → ℝ) x : ℝ)
      (((↑w : AbsoluteValue K ℝ) : (a : K) → ℝ) ((f : (a : k) → K) x : K) : ℝ)
a₄ a₅ :
  ∀ (x : k),
    Eq (α := ℝ) ((place (w.embedding.comp f) : (a : k) → ℝ) x : ℝ)
      ((place (⋯.choose (p := fun (φ : K →+* ℂ) ↦ place φ = (↑w : AbsoluteValue K ℝ))) : (a : K) → ℝ)
          ((f : (a : k) → K) x : K) :
        ℝ)
⊢ place (w.embedding.comp f) = (↑w : AbsoluteValue K ℝ).comp (f := f) ⋯

Tactic:
{ ext x; change _ = w.1 (f x); rw [← w.2.choose_spec]; rfl }

Premises used: Exists.choose_spec, Subtype.property
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
φ : K →+* ℂ
f : k →+* K
⊢ (mk φ).comap f = mk (φ.comp f)

Tactic:
rfl

Premises used: IsAbsoluteValue.toAbsoluteValue, NumberField.InfinitePlace.comap, NumberField.InfinitePlace.mk, AbsoluteValue.comp, NumberField.place, rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_2
inst : Field K
w : InfinitePlace K
⊢ w.comap (RingHom.id K) = w

Tactic:
rfl

Premises used: NumberField.InfinitePlace.comap, NumberField.InfinitePlace, AbsoluteValue.comp, rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
F : Type u_3
inst_2 : Field F
w : InfinitePlace K
f : F →+* K
g : k →+* F
⊢ w.comap (f.comp g) = (w.comap f).comap g

Tactic:
rfl

Premises used: NumberField.InfinitePlace.comap, NumberField.InfinitePlace, AbsoluteValue.comp, rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
w : InfinitePlace K
f : k →+* K
x : k
⊢ Eq (α := ℝ) ((w.comap f : (a : k) → ℝ) x : ℝ) ((w : (a : K) → ℝ) ((f : (a : k) → K) x : K) : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
v : InfinitePlace k
w : InfinitePlace K
f : k →+* K
h : w.comap f = v
x : k
⊢ Eq (α := ℝ) ((w : (a : K) → ℝ) ((f : (a : k) → K) x : K) : ℝ) ((v : (a : k) → ℝ) x : ℝ)

Tactic:
simp [← h]
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
ψ : K →+* ℂ
f : k →+* K
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := k) (β := K) (⇑f : (a : k) → K)
⊢ (↑(mk (ψ.comp f)) : AbsoluteValue k ℝ) = (↑(mk ψ) : AbsoluteValue K ℝ).comp h

Tactic:
rfl

Premises used: AbsoluteValue.comp, NumberField.place, rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : Algebra.IsAlgebraic k K
φ : k →+* ℂ
⊢ comap (mk (lift K φ)) (algebraMap k K) = mk φ

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
hφ : w.IsReal
rw : ComplexEmbedding.IsReal (w.embedding.comp f)
⊢ (w.comap f).IsReal

Tactic:
rw [← mk_embedding w, comap_mk, isReal_mk_iff]

Premises used: NumberField.InfinitePlace.comap_mk, NumberField.InfinitePlace.mk_embedding, NumberField.InfinitePlace.isReal_mk_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
hφ : w.IsReal
⊢ ComplexEmbedding.IsReal w.embedding

Tactic:
rw [← mk_embedding w, isReal_mk_iff] at hφ

Premises used: NumberField.InfinitePlace.mk_embedding, NumberField.InfinitePlace.isReal_mk_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
hφ : ComplexEmbedding.IsReal w.embedding
⊢ ComplexEmbedding.IsReal (w.embedding.comp f)

Tactic:
hφ.comp f

Premises used: NumberField.ComplexEmbedding.IsReal.comp
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
hφ : ComplexEmbedding.IsReal w.embedding
⊢ ComplexEmbedding.IsReal (w.embedding.comp f)

Tactic:
exact hφ.comp f

Premises used: NumberField.ComplexEmbedding.IsReal.comp
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
hf : (w.comap f).IsComplex
rw : ∀ (hf : ¬(w.comap f).IsReal), ¬w.IsReal
⊢ w.IsComplex

Tactic:
rw [← not_isReal_iff_isComplex] at hf ⊢

Premises used: NumberField.InfinitePlace.not_isReal_iff_isComplex
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
hf : ¬(w.comap f).IsReal
⊢ ¬w.IsReal

Tactic:
(IsReal.comap f).mt hf

Premises used: Function.mt, NumberField.InfinitePlace.IsReal.comap
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
hf : ¬(w.comap f).IsReal
⊢ ¬w.IsReal

Tactic:
exact (IsReal.comap f).mt hf

Premises used: Function.mt, NumberField.InfinitePlace.IsReal.comap
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k ≃+* K
w : InfinitePlace K
rw : IsReal ((mk w.embedding).comap (↑f : k →+* K)) ↔ (mk w.embedding).IsReal
rw₁ : IsReal (mk (w.embedding.comp (↑f : k →+* K))) ↔ (mk w.embedding).IsReal
rw₂ : ComplexEmbedding.IsReal (w.embedding.comp (↑f : k →+* K)) ↔ (mk w.embedding).IsReal
rw₃ : ComplexEmbedding.IsReal (w.embedding.comp (↑f : k →+* K)) ↔ ComplexEmbedding.IsReal w.embedding
rw₄ rw₅ : ComplexEmbedding.IsReal w.embedding ↔ ComplexEmbedding.IsReal w.embedding
⊢ IsReal (w.comap (↑f : k →+* K)) ↔ w.IsReal

Tactic:
rw [← mk_embedding w, comap_mk, isReal_mk_iff, isReal_mk_iff, ComplexEmbedding.isReal_comp_iff]

Premises used: NumberField.InfinitePlace.comap_mk, NumberField.InfinitePlace.mk_embedding, NumberField.InfinitePlace.isReal_mk_iff, NumberField.ComplexEmbedding.isReal_comp_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : Algebra.IsAlgebraic k K
w : InfinitePlace k
⊢ (fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) (mk (lift K w.embedding)) = w

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
h : (w.comap f).IsReal
rwa : (mk (w.embedding.comp f)).IsReal
rwa₁ : ((mk w.embedding).comap f).IsReal
rwa₂ rwa₃ rwa₄ rwa₅ : (w.comap f).IsReal
⊢ ComplexEmbedding.IsReal (w.embedding.comp f)

Tactic:
rwa [← isReal_mk_iff, ← comap_mk, mk_embedding]

Premises used: NumberField.InfinitePlace.comap_mk, NumberField.InfinitePlace.mk_embedding, NumberField.InfinitePlace.isReal_mk_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
h : (w.comap f).IsReal
rw : ((mk w.embedding).comap f).embedding = (mk w.embedding).embedding.comp f
rw₁ : (mk (w.embedding.comp f)).embedding = (mk w.embedding).embedding.comp f
rw₂ : (mk (w.embedding.comp f)).embedding = w.embedding.comp f
rw₃ rw₄ : w.embedding.comp f = w.embedding.comp f
⊢ (w.comap f).embedding = w.embedding.comp f

Tactic:
rw [← mk_embedding w, comap_mk, mk_embedding, embedding_mk_eq_of_isReal
    (by rwa [← isReal_mk_iff, ← comap_mk, mk_embedding])]

Premises used: NumberField.InfinitePlace.comap_mk, NumberField.InfinitePlace.mk_embedding, NumberField.InfinitePlace.embedding_mk_eq_of_isReal
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
pos : ∀ (h₁ : (w.comap f).IsReal) (h₂ : w.IsReal), LE.le (α := ℕ) 1 1
neg : ∀ (h₁ : (w.comap f).IsReal) (h₂ : ¬w.IsReal), LE.le (α := ℕ) 1 2
pos₁ : ∀ (h₁ : ¬(w.comap f).IsReal) (h₂ : w.IsReal), LE.le (α := ℕ) 2 1
neg₁ : ∀ (h₁ : ¬(w.comap f).IsReal) (h₂ : ¬w.IsReal), LE.le (α := ℕ) 2 2
⊢ LE.le (α := ℕ) (if (w.comap f).IsReal then 1 else 2) (if w.IsReal then 1 else 2)

Tactic:
split_ifs with h₁ h₂ h₂
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
h₁ : ¬(w.comap f).IsReal
h₂ : w.IsReal
⊢ LE.le (α := ℕ) 2 1

Tactic:
(h₁ (h₂.comap _)).elim

Premises used: False.elim, NumberField.InfinitePlace.IsReal.comap
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
h₁ : ¬(w.comap f).IsReal
h₂ : w.IsReal
⊢ LE.le (α := ℕ) 2 1

Tactic:
exact (h₁ (h₂.comap _)).elim

Premises used: False.elim, NumberField.InfinitePlace.IsReal.comap
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
h₁ : (w.comap f).IsReal
h₂ : w.IsReal
⊢ LE.le (α := ℕ) 1 1

Tactic:
decide
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
h₁ : (w.comap f).IsReal
h₂ : ¬w.IsReal
⊢ LE.le (α := ℕ) 1 2

Tactic:
decide
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
h₁ : ¬(w.comap f).IsReal
h₂ : ¬w.IsReal
⊢ LE.le (α := ℕ) 2 2

Tactic:
decide