awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_3 : Algebra k K
inst_4 : Algebra k F
inst_5 : Algebra K F
inst_6 : IsScalarTower k K F
w : InfinitePlace F
h : IsUnramified k w
⊢ mult (comap (w.comap (algebraMap K F)) (algebraMap k K)) ≤ mult (w.comap (algebraMap K F))

Tactic:
exact InfinitePlace.mult_comap_le _ _

Premises used: NumberField.InfinitePlace.mult_comap_le
-- 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
inst_3 : Algebra k K
inst_4 : Algebra k F
inst_5 : Algebra K F
inst_6 : IsScalarTower k K F
w : InfinitePlace F
h : IsUnramified k w
⊢ IsUnramified k (w.comap (algebraMap K F))

Tactic:
h.comap_algHom (IsScalarTower.toAlgHom k K F)

Premises used: NumberField.InfinitePlace.IsUnramified.comap_algHom, IsScalarTower.toAlgHom, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom
-- 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
w : InfinitePlace K
rw :
  ¬Eq (α := ℕ) (if IsReal (w.comap (algebraMap k K)) then 1 else 2) (if w.IsReal then 1 else 2) ↔
    ¬w.IsReal ∧ IsReal (w.comap (algebraMap k K))
⊢ ¬IsUnramified k w ↔ w.IsComplex ∧ IsReal (w.comap (algebraMap k K))

Tactic:
rw [IsUnramified, mult, mult, ← not_isReal_iff_isComplex]

Premises used: NumberField.InfinitePlace.mult, NumberField.InfinitePlace.IsUnramified, 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
inst_2 : Algebra k K
w : InfinitePlace K
pos :
  ∀ (h₁ : IsReal (w.comap (algebraMap k K))) (h₂ : w.IsReal),
    ¬Eq (α := ℕ) 1 1 ↔ ¬w.IsReal ∧ IsReal (w.comap (algebraMap k K))
neg :
  ∀ (h₁ : IsReal (w.comap (algebraMap k K))) (h₂ : ¬w.IsReal),
    ¬Eq (α := ℕ) 1 2 ↔ ¬w.IsReal ∧ IsReal (w.comap (algebraMap k K))
pos₁ :
  ∀ (h₁ : ¬IsReal (w.comap (algebraMap k K))) (h₂ : w.IsReal),
    ¬Eq (α := ℕ) 2 1 ↔ ¬w.IsReal ∧ IsReal (w.comap (algebraMap k K))
neg₁ :
  ∀ (h₁ : ¬IsReal (w.comap (algebraMap k K))) (h₂ : ¬w.IsReal),
    ¬Eq (α := ℕ) 2 2 ↔ ¬w.IsReal ∧ IsReal (w.comap (algebraMap k K))
⊢ ¬Eq (α := ℕ) (if IsReal (w.comap (algebraMap k K)) then 1 else 2) (if w.IsReal then 1 else 2) ↔
    ¬w.IsReal ∧ IsReal (w.comap (algebraMap k K))

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
inst_2 : Algebra k K
w : InfinitePlace K
h₁ : IsReal (w.comap (algebraMap k K))
h₂ : w.IsReal
⊢ ¬Eq (α := ℕ) 1 1 ↔ ¬w.IsReal ∧ IsReal (w.comap (algebraMap k K))

Tactic:
simp only [not_true_eq_false, false_iff, and_self, forall_true_left, IsEmpty.forall_iff,
      not_and, OfNat.one_ne_ofNat, not_false_eq_true, true_iff, OfNat.ofNat_ne_one, h₁, h₂]

Premises used: forall_true_left, OfNat.one_ne_ofNat, and_self, OfNat.ofNat_ne_one, true_iff, not_true_eq_false, false_iff, not_false_eq_true, not_and, IsEmpty.forall_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
w : InfinitePlace K
h₁ : IsReal (w.comap (algebraMap k K))
h₂ : ¬w.IsReal
⊢ ¬Eq (α := ℕ) 1 2 ↔ ¬w.IsReal ∧ IsReal (w.comap (algebraMap k K))

Tactic:
simp only [not_true_eq_false, false_iff, and_self, forall_true_left, IsEmpty.forall_iff,
      not_and, OfNat.one_ne_ofNat, not_false_eq_true, true_iff, OfNat.ofNat_ne_one, h₁, h₂]

Premises used: forall_true_left, OfNat.one_ne_ofNat, and_self, OfNat.ofNat_ne_one, true_iff, not_true_eq_false, false_iff, not_false_eq_true, not_and, IsEmpty.forall_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
w : InfinitePlace K
h₁ : ¬IsReal (w.comap (algebraMap k K))
h₂ : w.IsReal
pos : False
⊢ ¬Eq (α := ℕ) 2 1 ↔ ¬w.IsReal ∧ IsReal (w.comap (algebraMap k K))

Tactic:
simp only [not_true_eq_false, false_iff, and_self, forall_true_left, IsEmpty.forall_iff,
      not_and, OfNat.one_ne_ofNat, not_false_eq_true, true_iff, OfNat.ofNat_ne_one, h₁, h₂]

Premises used: forall_true_left, OfNat.one_ne_ofNat, and_self, OfNat.ofNat_ne_one, true_iff, not_true_eq_false, false_iff, not_false_eq_true, not_and, IsEmpty.forall_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
w : InfinitePlace K
h₁ : ¬IsReal (w.comap (algebraMap k K))
h₂ : ¬w.IsReal
⊢ ¬Eq (α := ℕ) 2 2 ↔ ¬w.IsReal ∧ IsReal (w.comap (algebraMap k K))

Tactic:
simp only [not_true_eq_false, false_iff, and_self, forall_true_left, IsEmpty.forall_iff,
      not_and, OfNat.one_ne_ofNat, not_false_eq_true, true_iff, OfNat.ofNat_ne_one, h₁, h₂]

Premises used: forall_true_left, OfNat.one_ne_ofNat, and_self, OfNat.ofNat_ne_one, true_iff, not_true_eq_false, false_iff, not_false_eq_true, not_and, IsEmpty.forall_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
w : InfinitePlace K
h₁ : ¬IsReal (w.comap (algebraMap k K))
h₂ : w.IsReal
⊢ False

Tactic:
h₁ (h₂.comap _)

Premises used: 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
inst_2 : Algebra k K
w : InfinitePlace K
h₁ : ¬IsReal (w.comap (algebraMap k K))
h₂ : w.IsReal
⊢ False

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

Premises used: 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
inst_2 : Algebra k K
w : InfinitePlace K
rw : ¬IsUnramified k w ↔ ¬(w.IsReal ∨ IsComplex (w.comap (algebraMap k K)))
rw₁ : w.IsComplex ∧ IsReal (w.comap (algebraMap k K)) ↔ ¬(w.IsReal ∨ IsComplex (w.comap (algebraMap k K)))
rw₂ : w.IsComplex ∧ IsReal (w.comap (algebraMap k K)) ↔ ¬w.IsReal ∧ ¬IsComplex (w.comap (algebraMap k K))
rw₃ : w.IsComplex ∧ IsReal (w.comap (algebraMap k K)) ↔ w.IsComplex ∧ ¬IsComplex (w.comap (algebraMap k K))
rw₄ rw₅ : w.IsComplex ∧ IsReal (w.comap (algebraMap k K)) ↔ w.IsComplex ∧ IsReal (w.comap (algebraMap k K))
⊢ IsUnramified k w ↔ w.IsReal ∨ IsComplex (w.comap (algebraMap k K))

Tactic:
rw [← not_iff_not, not_isUnramified_iff, not_or,
    not_isReal_iff_isComplex, not_isComplex_iff_isReal]

Premises used: not_iff_not, NumberField.InfinitePlace.not_isComplex_iff_isReal, not_or, NumberField.InfinitePlace.not_isUnramified_iff, 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
inst_2 : Algebra k K
w : InfinitePlace K
⊢ IsRamified k w ↔ w.IsComplex ∧ IsReal (w.comap (algebraMap k K))

Tactic:
not_isUnramified_iff

Premises used: NumberField.InfinitePlace.not_isUnramified_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
w : InfinitePlace K
h : IsRamified k w
⊢ w.IsComplex

Tactic:
(isRamified_iff.1 h).1

Premises used: NumberField.InfinitePlace.isRamified_iff, And.left, Iff.mp
-- 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
w : InfinitePlace K
h : IsRamified k w
⊢ IsReal (w.comap (algebraMap k K))

Tactic:
(isRamified_iff.1 h).2

Premises used: NumberField.InfinitePlace.isRamified_iff, And.right, Iff.mp
-- 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
w₁ w₂ : InfinitePlace K
h : IsRamified k w₂
pos : ∀ (h_eq : w₁ = w₂), w₁.embedding ≠ conjugate w₂.embedding
neg : ∀ (h_eq : ¬w₁ = w₂), w₁.embedding ≠ conjugate w₂.embedding
⊢ w₁.embedding ≠ conjugate w₂.embedding

Tactic:
by_cases h_eq : w₁ = w₂
-- 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
w₁ w₂ : InfinitePlace K
h : IsRamified k w₂
h_eq : w₁ = w₂
⊢ ¬ComplexEmbedding.IsReal w₂.embedding ∧ IsReal (w₂.comap (algebraMap k K))

Tactic:
rw [isRamified_iff, isComplex_iff] at h

Premises used: NumberField.InfinitePlace.isRamified_iff, NumberField.InfinitePlace.isComplex_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
w₁ w₂ : InfinitePlace K
h : IsRamified k w₂
h_eq : w₁ = w₂
h₁ : ¬ComplexEmbedding.IsReal w₂.embedding ∧ IsReal (w₂.comap (algebraMap k K))
⊢ w₁ = w₂

Tactic:
rw [isRamified_iff, isComplex_iff] at h

Premises used: NumberField.InfinitePlace.isRamified_iff, NumberField.InfinitePlace.isComplex_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
w₁ w₂ : InfinitePlace K
h : ¬ComplexEmbedding.IsReal w₂.embedding ∧ IsReal (w₂.comap (algebraMap k K))
h_eq : w₁ = w₂
⊢ w₁.embedding ≠ conjugate w₂.embedding

Tactic:
Ne.symm (h_eq ▸ h.1)

Premises used: Eq.rec, Ne.symm, And.left, Eq.symm
-- 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
w₁ w₂ : InfinitePlace K
h : ¬ComplexEmbedding.IsReal w₂.embedding ∧ IsReal (w₂.comap (algebraMap k K))
h_eq : w₁ = w₂
⊢ w₁.embedding ≠ conjugate w₂.embedding

Tactic:
exact Ne.symm (h_eq ▸ h.1)

Premises used: Ne.symm
-- 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
w₁ w₂ : InfinitePlace K
h : IsRamified k w₂
h_eq : ¬w₁ = w₂
neg : ∀ (h_eq : w₁.embedding = conjugate w₂.embedding), w₁ = w₂
⊢ w₁.embedding ≠ conjugate w₂.embedding

Tactic:
contrapose h_eq
-- 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
w₁ w₂ : InfinitePlace K
h : IsRamified k w₂
h_eq : w₁.embedding = conjugate w₂.embedding
neg : mk w₁.embedding = w₂
neg₁ : mk (conjugate w₂.embedding) = w₂
neg₂ : mk w₂.embedding = w₂
neg₃ neg₄ : w₂ = w₂
⊢ w₁ = w₂

Tactic:
rw [← mk_embedding w₁, h_eq, mk_conjugate_eq, mk_embedding]

Premises used: NumberField.InfinitePlace.mk_embedding, NumberField.InfinitePlace.mk_conjugate_eq
-- 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
w : InfinitePlace K
h : IsRamified k w
rw rw₁ : Eq (α := k →+* ℂ) (embedding (w.comap (algebraMap k K))) (embedding (w.comap (algebraMap k K)))
⊢ Eq (α := k →+* ℂ) (embedding (w.comap (algebraMap k K))) (w.embedding.comp (algebraMap k K))

Tactic:
rw [← comap_embedding_of_isReal _ (isRamified_iff.1 h).2]

Premises used: NumberField.InfinitePlace.isRamified_iff, And.right, Iff.mp, NumberField.InfinitePlace.comap_embedding_of_isReal
-- 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
w : InfinitePlace K
h : IsRamified k w
rw :
  Eq (α := k →+* ℂ) (conjugate (embedding (w.comap (algebraMap k K)))) ((conjugate w.embedding).comp (algebraMap k K))
⊢ Eq (α := k →+* ℂ) (embedding (w.comap (algebraMap k K))) ((conjugate w.embedding).comp (algebraMap k K))

Tactic:
rw [← ComplexEmbedding.isReal_iff.1 <| isReal_iff.1 ((isRamified_iff.1 h).2)]

Premises used: NumberField.InfinitePlace.isReal_iff, NumberField.InfinitePlace.isRamified_iff, And.right, Iff.mp, NumberField.ComplexEmbedding.isReal_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
w : InfinitePlace K
h : IsRamified k w
⊢ Eq (α := k →+* ℂ) (conjugate (embedding (w.comap (algebraMap k K)))) ((conjugate w.embedding).comp (algebraMap k K))

Tactic:
simp [conjugate_comp, comap_embedding_of_isReal _ ((isRamified_iff.1 h).2)]

Premises used: NumberField.ComplexEmbedding.conjugate_comp, NumberField.InfinitePlace.isRamified_iff, And.right, Iff.mp, NumberField.InfinitePlace.comap_embedding_of_isReal
-- 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
w : InfinitePlace K
h : IsRamified k w
⊢ IsMixed k w.embedding

Tactic:
⟨comap_embedding_of_isReal _ h.isReal ▸ isReal_iff.1 h.isReal, isComplex_iff.1 h.isComplex⟩

Premises used: NumberField.InfinitePlace.IsRamified.isComplex, NumberField.InfinitePlace.isReal_iff, Eq.rec, NumberField.InfinitePlace.IsRamified.isReal, And.intro, NumberField.InfinitePlace.isComplex_iff, Iff.mp, NumberField.InfinitePlace.comap_embedding_of_isReal
-- 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
w : InfinitePlace K
h : IsRamified k w
⊢ ¬ComplexEmbedding.IsReal (conjugate w.embedding)

Tactic:
simpa using isComplex_iff.1 <| h.isComplex

Premises used: NumberField.InfinitePlace.IsRamified.isComplex, NumberField.InfinitePlace.isComplex_iff, Iff.mp
-- 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
φ : K →+* ℂ
⊢ IsRamified k (mk φ) ↔ IsMixed k φ

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- 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
φ : K →+* ℂ
refine_1 : ∀ (h : IsRamified k (mk φ)), IsMixed k φ
refine_2 : ∀ (h : IsMixed k φ), IsRamified k (mk φ)
⊢ IsRamified k (mk φ) ↔ IsMixed k φ

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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
φ : K →+* ℂ
h : IsRamified k (mk φ)
refine_1 : ∀ (hl : (mk φ).embedding = φ), IsMixed k φ
refine_1₁ : ∀ (hr : (mk φ).embedding = conjugate φ), IsMixed k φ
⊢ IsMixed k φ

Tactic:
rcases embedding_mk_eq φ with (hl | hr)

Premises used: NumberField.InfinitePlace.embedding_mk_eq
-- 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
φ : K →+* ℂ
h : IsRamified k (mk φ)
hl : (mk φ).embedding = φ
⊢ IsMixed k φ

Tactic:
hl ▸ h.isMixed_embedding

Premises used: Eq.rec, NumberField.InfinitePlace.IsRamified.isMixed_embedding
-- 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
φ : K →+* ℂ
h : IsRamified k (mk φ)
hl : (mk φ).embedding = φ
⊢ IsMixed k φ

Tactic:
exact hl ▸ h.isMixed_embedding
-- 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
φ : K →+* ℂ
h : IsRamified k (mk φ)
hr : (mk φ).embedding = conjugate φ
refine_1 : IsMixed k (star (star φ))
⊢ IsMixed k φ

Tactic:
rw [← star_star φ]

Premises used: star_star
-- 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
φ : K →+* ℂ
h : IsRamified k (mk φ)
hr : (mk φ).embedding = conjugate φ
⊢ IsMixed k (star (star φ))

Tactic:
simpa [← congrArg conjugate hr] using h.isMixed_conjugate_embedding

Premises used: NumberField.ComplexEmbedding.conjugate, congrArg, NumberField.InfinitePlace.IsRamified.isMixed_conjugate_embedding
-- 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
φ : K →+* ℂ
h : IsMixed k φ
refine_2 : ¬ComplexEmbedding.IsReal (mk φ).embedding ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
⊢ IsRamified k (mk φ)

Tactic:
rw [isRamified_iff, isComplex_iff, comap_mk, isReal_iff, embedding_mk_eq_of_isReal h.1]

Premises used: NumberField.InfinitePlace.comap_mk, NumberField.InfinitePlace.isReal_iff, NumberField.InfinitePlace.isRamified_iff, NumberField.InfinitePlace.embedding_mk_eq_of_isReal, And.left, NumberField.InfinitePlace.isComplex_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
φ : K →+* ℂ
h : IsMixed k φ
inl : (mk φ).embedding = φ → ¬ComplexEmbedding.IsReal (mk φ).embedding
inr : (mk φ).embedding = conjugate φ → ¬ComplexEmbedding.IsReal (mk φ).embedding
⊢ ¬ComplexEmbedding.IsReal (mk φ).embedding

Tactic:
rcases embedding_mk_eq φ with (_ | _)

Premises used: NumberField.InfinitePlace.embedding_mk_eq
-- 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
φ : K →+* ℂ
h : IsMixed k φ
h_1 : (mk φ).embedding = φ
⊢ ¬ComplexEmbedding.IsReal (mk φ).embedding

Tactic:
aesop
-- 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
φ : K →+* ℂ
h : IsMixed k φ
h_1 : (mk φ).embedding = conjugate φ
⊢ ¬ComplexEmbedding.IsReal (mk φ).embedding

Tactic:
aesop
-- 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
φ : K →+* ℂ
h : IsMixed k φ
⊢ ¬ComplexEmbedding.IsReal (mk φ).embedding ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))

Tactic:
exact ⟨by rcases embedding_mk_eq φ with (_ | _) <;> aesop, h.1⟩
-- 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
w : InfinitePlace K
h : IsUnramified k w
hw : ComplexEmbedding.IsReal (w.embedding.comp (algebraMap k K))
⊢ IsReal (w.comap (algebraMap k K))

Tactic:
rw [← isReal_mk_iff, ← comap_mk, mk_embedding] at hw

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
inst_2 : Algebra k K
w : InfinitePlace K
h : IsUnramified k w
hw : IsReal (w.comap (algebraMap k K))
⊢ ComplexEmbedding.IsReal w.embedding

Tactic:
isReal_iff.1 <| (isUnramified_iff.1 h).resolve_right (not_isComplex_iff_isReal.2 hw)

Premises used: Iff.mpr, NumberField.InfinitePlace.not_isComplex_iff_isReal, NumberField.InfinitePlace.isReal_iff, NumberField.InfinitePlace.isUnramified_iff, Iff.mp, Or.resolve_right
-- 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
w : InfinitePlace K
h : IsUnramified k w
hw : IsReal (w.comap (algebraMap k K))
⊢ ComplexEmbedding.IsReal w.embedding

Tactic:
exact isReal_iff.1 <| (isUnramified_iff.1 h).resolve_right (not_isComplex_iff_isReal.2 hw)

Premises used: Iff.mpr, NumberField.InfinitePlace.not_isComplex_iff_isReal, NumberField.InfinitePlace.isReal_iff, NumberField.InfinitePlace.isUnramified_iff, Iff.mp, Or.resolve_right
-- 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
w : InfinitePlace K
h : IsUnramified k w
hw : ComplexEmbedding.IsReal ((conjugate w.embedding).comp (algebraMap k K))
⊢ IsReal (w.comap (algebraMap k K))

Tactic:
simp_rw [conjugate_comp, IsSelfAdjoint.star_iff, ← isReal_mk_iff, ← comap_mk, mk_embedding] at hw

Premises used: NumberField.InfinitePlace.comap_mk, NumberField.ComplexEmbedding.conjugate_comp, NumberField.InfinitePlace.mk_embedding, NumberField.InfinitePlace.isReal_mk_iff, IsSelfAdjoint.star_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
w : InfinitePlace K
h : IsUnramified k w
hw : IsReal (w.comap (algebraMap k K))
⊢ ComplexEmbedding.IsReal (conjugate w.embedding)

Tactic:
simpa using isReal_iff.1 <| (isUnramified_iff.1 h).resolve_right (not_isComplex_iff_isReal.2 hw)

Premises used: Iff.mpr, NumberField.InfinitePlace.not_isComplex_iff_isReal, NumberField.InfinitePlace.isReal_iff, NumberField.InfinitePlace.isUnramified_iff, Iff.mp, Or.resolve_right
-- 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
φ : K →+* ℂ
⊢ IsUnramified k (mk φ) ↔ IsUnmixed k φ

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- 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
φ : K →+* ℂ
refine_1 : ∀ (h : IsUnramified k (mk φ)), IsUnmixed k φ
refine_2 : ∀ (h : IsUnmixed k φ), IsUnramified k (mk φ)
⊢ IsUnramified k (mk φ) ↔ IsUnmixed k φ

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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
φ : K →+* ℂ
h : IsUnramified k (mk φ)
refine_1 : ∀ (hl : (mk φ).embedding = φ), IsUnmixed k φ
refine_1₁ : ∀ (hr : (mk φ).embedding = conjugate φ), IsUnmixed k φ
⊢ IsUnmixed k φ

Tactic:
rcases embedding_mk_eq φ with (hl | hr)

Premises used: NumberField.InfinitePlace.embedding_mk_eq
-- 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
φ : K →+* ℂ
h : IsUnramified k (mk φ)
hl : (mk φ).embedding = φ
⊢ IsUnmixed k φ

Tactic:
hl ▸ h.isUnmixed

Premises used: NumberField.InfinitePlace.IsUnramified.isUnmixed, Eq.rec
-- 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
φ : K →+* ℂ
h : IsUnramified k (mk φ)
hl : (mk φ).embedding = φ
⊢ IsUnmixed k φ

Tactic:
exact hl ▸ h.isUnmixed
-- 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
φ : K →+* ℂ
h : IsUnramified k (mk φ)
hr : (mk φ).embedding = conjugate φ
refine_1 : IsUnmixed k (star (star φ))
⊢ IsUnmixed k φ

Tactic:
rw [← star_star φ]

Premises used: star_star
-- 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
φ : K →+* ℂ
h : IsUnramified k (mk φ)
hr : (mk φ).embedding = conjugate φ
⊢ IsUnmixed k (star (star φ))

Tactic:
simpa [← congrArg conjugate hr] using h.isUnmixed_conjugate

Premises used: NumberField.InfinitePlace.IsUnramified.isUnmixed_conjugate, NumberField.ComplexEmbedding.conjugate, congrArg
-- 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
φ : K →+* ℂ
h : IsUnmixed k φ
refine_2 : ComplexEmbedding.IsReal (mk φ).embedding ∨ IsComplex ((mk φ).comap (algebraMap k K))
⊢ IsUnramified k (mk φ)

Tactic:
rw [isUnramified_iff, isReal_iff]

Premises used: NumberField.InfinitePlace.isReal_iff, NumberField.InfinitePlace.isUnramified_iff