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
inst_2 : Algebra k K
inst_3 : IsGalois k K
h : Odd (Nat.card.{u_2} Gal(K/k))
⊢ IsUnramifiedAtInfinitePlaces k K

Tactic:
⟨fun _ ↦ not_not.mp (Nat.not_even_iff_odd.2 h ∘ InfinitePlace.even_card_aut_of_not_isUnramified)⟩

Premises used: Iff.mpr, Classical.not_not, Function.comp, NumberField.InfinitePlace.even_card_aut_of_not_isUnramified, Nat.not_even_iff_odd, Iff.mp, IsUnramifiedAtInfinitePlaces.mk
-- 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 : IsGalois k K
h : Odd (finrank k K)
⊢ IsUnramifiedAtInfinitePlaces k K

Tactic:
⟨fun _ ↦ not_not.mp (Nat.not_even_iff_odd.2 h ∘ InfinitePlace.even_finrank_of_not_isUnramified)⟩

Premises used: Iff.mpr, Classical.not_not, Function.comp, Nat.not_even_iff_odd, NumberField.InfinitePlace.even_finrank_of_not_isUnramified, Iff.mp, IsUnramifiedAtInfinitePlaces.mk
-- 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 : NumberField k
inst_4 : NumberField K
inst_5 : IsGalois k K
inst_6 : IsUnramifiedAtInfinitePlaces k K
rw : Eq.{u_1 + 1} (α := Finset (InfinitePlace k)) Finset.univᶜ ∅
rw₁ :
  ∀ (x : InfinitePlace k),
    Membership.mem (γ := Finset (InfinitePlace k)) Finset.univ x → InfinitePlace.IsUnramifiedIn K x
⊢ card.{u_2} (InfinitePlace K) = card.{u_1} (InfinitePlace k) * finrank k K

Tactic:
rw [InfinitePlace.card_eq_card_isUnramifiedIn (k := k) (K := K), Finset.filter_true_of_mem,
    Finset.card_univ, Finset.card_eq_zero.mpr, zero_mul, add_zero]

Premises used: Iff.mpr, Finset.card_univ, MulZeroClass.zero_mul, NumberField.InfinitePlace.card_eq_card_isUnramifiedIn, Finset.filter_true_of_mem, Finset.card_eq_zero, add_zero
-- 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 : NumberField k
inst_4 : NumberField K
inst_5 : IsGalois k K
inst_6 : IsUnramifiedAtInfinitePlaces k K
⊢ Eq.{u_1 + 1} (α := Finset (InfinitePlace k)) Finset.univᶜ ∅

Tactic:
Finset.compl_univ

Premises used: Finset.compl_univ
-- 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 : NumberField k
inst_4 : NumberField K
inst_5 : IsGalois k K
inst_6 : IsUnramifiedAtInfinitePlaces k K
⊢ Eq.{u_1 + 1} (α := Finset (InfinitePlace k)) Finset.univᶜ ∅

Tactic:
exact Finset.compl_univ

Premises used: Finset.compl_univ
-- 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 : NumberField k
inst_4 : NumberField K
inst_5 : IsGalois k K
inst_6 : IsUnramifiedAtInfinitePlaces k K
simp : ∀ (x : InfinitePlace k), InfinitePlace.IsUnramifiedIn K x
⊢ ∀ (x : InfinitePlace k),
    Membership.mem (γ := Finset (InfinitePlace k)) Finset.univ x → InfinitePlace.IsUnramifiedIn K x

Tactic:
simp only [Finset.mem_univ, forall_true_left]

Premises used: Finset.mem_univ, forall_true_left
-- 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 : NumberField k
inst_4 : NumberField K
inst_5 : IsGalois k K
inst_6 : IsUnramifiedAtInfinitePlaces k K
⊢ ∀ (x : InfinitePlace k), InfinitePlace.IsUnramifiedIn K x

Tactic:
InfinitePlace.isUnramifiedIn K

Premises used: NumberField.InfinitePlace.isUnramifiedIn
-- 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 : NumberField k
inst_4 : NumberField K
inst_5 : IsGalois k K
inst_6 : IsUnramifiedAtInfinitePlaces k K
⊢ ∀ (x : InfinitePlace k), InfinitePlace.IsUnramifiedIn K x

Tactic:
exact InfinitePlace.isUnramifiedIn K

Premises used: NumberField.InfinitePlace.isUnramifiedIn
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
k : Type u_1
inst : Field k
K_1 : Type u_2
inst_1 : Field K_1
F : Type u_3
inst_2 : Field F
inst_3 : Algebra k K_1
inst_4 : Algebra k F
inst_5 : Algebra K_1 F
inst_6 : IsScalarTower k K_1 F
K : Type u_4
L : Type u_5
inst_7 : Field K
inst_8 : Field L
inst_9 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_10 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
φ : K →+* ℂ
ψ : L →+* ℂ
inst_11 : ComplexEmbedding.LiesOver ψ φ
⊢ (↑(mk ψ) : AbsoluteValue L ℝ).comp (f := algebraMap K L) ⋯ = (↑(mk φ) : AbsoluteValue K ℝ)

Tactic:
simp [← LiesOver.over ψ φ, ← coe_mk_comp]

Premises used: NumberField.InfinitePlace.coe_mk_comp, NumberField.ComplexEmbedding.LiesOver.over
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
h : ∀ (k : K), Eq (α := ℝ) ((w.comap (algebraMap K L) : (a : K) → ℝ) k : ℝ) ((v : (a : K) → ℝ) k : ℝ)
⊢ w.comap (algebraMap K L) = v

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
k : K
⊢ Eq (α := ℝ) ((w.comap (algebraMap K L) : (a : K) → ℝ) k : ℝ) ((v : (a : K) → ℝ) k : ℝ)

Tactic:
simpa only [coe_apply] using AbsoluteValue.ext_iff.1 (LiesOver.comp_eq w.1 v.1) _

Premises used: NumberField.InfinitePlace.coe_apply, AbsoluteValue.ext_iff, AbsoluteValue.LiesOver.comp_eq, Iff.mp, Subtype.val
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
rw : (mk w.embedding).comap (algebraMap K L) = v
rw₁ : w.comap (algebraMap K L) = v
rw₂ rw₃ : v = v
⊢ mk (w.embedding.comp (algebraMap K L)) = v

Tactic:
rw [← comap_mk, w.mk_embedding, comap_eq w v]

Premises used: NumberField.InfinitePlace.comap_mk, NumberField.InfinitePlace.mk_embedding, NumberField.InfinitePlace.LiesOver.comap_eq
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
hl : Eq (α := K →+* ℂ) (embedding (mk (w.embedding.comp (algebraMap K L)))) (w.embedding.comp (algebraMap K L))
⊢ w.embedding.comp (algebraMap K L) = v.embedding ∨ (conjugate w.embedding).comp (algebraMap K L) = v.embedding

Tactic:
.inl (hl ▸ congrArg embedding (mk_embedding_comp w v))

Premises used: congrArg, Eq.rec, NumberField.InfinitePlace.embedding, NumberField.InfinitePlace.LiesOver.mk_embedding_comp, Or.inl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
hl : Eq (α := K →+* ℂ) (embedding (mk (w.embedding.comp (algebraMap K L)))) (w.embedding.comp (algebraMap K L))
⊢ w.embedding.comp (algebraMap K L) = v.embedding ∨ (conjugate w.embedding).comp (algebraMap K L) = v.embedding

Tactic:
exact .inl (hl ▸ congrArg embedding (mk_embedding_comp w v))
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
hr :
  Eq (α := K →+* ℂ) (embedding (mk (w.embedding.comp (algebraMap K L)))) (conjugate (w.embedding.comp (algebraMap K L)))
⊢ w.embedding.comp (algebraMap K L) = v.embedding ∨ (conjugate w.embedding).comp (algebraMap K L) = v.embedding

Tactic:
simpa using .inr (hr ▸ congrArg embedding (mk_embedding_comp w v))
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
⊢ Eq (α := K →+* ℂ) (embedding (mk (w.embedding.comp (algebraMap K L)))) (w.embedding.comp (algebraMap K L)) ∨
    Eq (α := K →+* ℂ) (embedding (mk (w.embedding.comp (algebraMap K L))))
      (conjugate (w.embedding.comp (algebraMap K L)))

Tactic:
cases embedding_mk_eq (w.embedding.comp (algebraMap K L)) with
  | inl hl => exact .inl (hl ▸ congrArg embedding (mk_embedding_comp w v))
  | inr hr => simpa using .inr (hr ▸ congrArg embedding (mk_embedding_comp w v))

Premises used: Algebra.algebraMap, NumberField.InfinitePlace.embedding, RingHom.comp, NumberField.InfinitePlace.embedding_mk_eq
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
hv : v.IsComplex
rw :
  ∀ (hv : ∃ (x : K), ¬Eq (α := ℂ) ((conjugate v.embedding : (a : K) → ℂ) x : ℂ) ((v.embedding : (a : K) → ℂ) x : ℂ)),
    ∃ (x : L), ¬Eq (α := ℂ) ((conjugate w.embedding : (a : L) → ℂ) x : ℂ) ((w.embedding : (a : L) → ℂ) x : ℂ)
⊢ w.IsComplex

Tactic:
rw [isComplex_iff, ComplexEmbedding.isReal_iff, RingHom.ext_iff, not_forall] at hv ⊢

Premises used: RingHom.ext_iff, NumberField.InfinitePlace.isComplex_iff, NumberField.ComplexEmbedding.isReal_iff, Classical.not_forall
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
hv : ∃ (x : K), ¬Eq (α := ℂ) ((conjugate v.embedding : (a : K) → ℂ) x : ℂ) ((v.embedding : (a : K) → ℂ) x : ℂ)
obtain :
  ∀ (x : K) (hx : ¬Eq (α := ℂ) ((conjugate v.embedding : (a : K) → ℂ) x : ℂ) ((v.embedding : (a : K) → ℂ) x : ℂ)),
    ∃ (x : L), ¬Eq (α := ℂ) ((conjugate w.embedding : (a : L) → ℂ) x : ℂ) ((w.embedding : (a : L) → ℂ) x : ℂ)
⊢ ∃ (x : L), ¬Eq (α := ℂ) ((conjugate w.embedding : (a : L) → ℂ) x : ℂ) ((w.embedding : (a : L) → ℂ) x : ℂ)

Tactic:
obtain ⟨x, hx⟩ := hv
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
x : K
hx : ¬Eq (α := ℂ) ((conjugate v.embedding : (a : K) → ℂ) x : ℂ) ((v.embedding : (a : K) → ℂ) x : ℂ)
h :
  ¬Eq (α := ℂ) ((conjugate w.embedding : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ)
      ((w.embedding : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ)
⊢ ∃ (x : L), ¬Eq (α := ℂ) ((conjugate w.embedding : (a : L) → ℂ) x : ℂ) ((w.embedding : (a : L) → ℂ) x : ℂ)

Tactic:
use algebraMap K L x

Premises used: Algebra.algebraMap, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
x : K
hx : ¬Eq (α := ℂ) ((conjugate v.embedding : (a : K) → ℂ) x : ℂ) ((v.embedding : (a : K) → ℂ) x : ℂ)
⊢ ¬Eq (α := ℂ) ((conjugate (embedding (mk (w.embedding.comp (algebraMap K L)))) : (a : K) → ℂ) x : ℂ)
      ((embedding (mk (w.embedding.comp (algebraMap K L))) : (a : K) → ℂ) x : ℂ)

Tactic:
rw [← comap_eq w v, ← mk_embedding w, comap_mk] at hx

Premises used: NumberField.InfinitePlace.comap_mk, NumberField.InfinitePlace.mk_embedding, NumberField.InfinitePlace.LiesOver.comap_eq
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
x : K
hx :
  ¬Eq (α := ℂ) ((conjugate (embedding (mk (w.embedding.comp (algebraMap K L)))) : (a : K) → ℂ) x : ℂ)
      ((embedding (mk (w.embedding.comp (algebraMap K L))) : (a : K) → ℂ) x : ℂ)
h :
  Eq (α := K →+* ℂ) (embedding (mk (w.embedding.comp (algebraMap K L)))) (w.embedding.comp (algebraMap K L)) →
    ¬Eq (α := ℂ) ((conjugate w.embedding : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ)
        ((w.embedding : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ)
h₁ :
  Eq (α := K →+* ℂ) (embedding (mk (w.embedding.comp (algebraMap K L))))
      (conjugate (w.embedding.comp (algebraMap K L))) →
    ¬Eq (α := ℂ) ((conjugate w.embedding : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ)
        ((w.embedding : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ)
⊢ ¬Eq (α := ℂ) ((conjugate w.embedding : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ)
      ((w.embedding : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ)

Tactic:
rcases embedding_mk_eq (w.embedding.comp (algebraMap K L)) with (_ | _)

Premises used: Algebra.algebraMap, NumberField.InfinitePlace.embedding, RingHom.comp, NumberField.InfinitePlace.embedding_mk_eq
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
x : K
hx :
  ¬Eq (α := ℂ) ((conjugate (embedding (mk (w.embedding.comp (algebraMap K L)))) : (a : K) → ℂ) x : ℂ)
      ((embedding (mk (w.embedding.comp (algebraMap K L))) : (a : K) → ℂ) x : ℂ)
h : Eq (α := K →+* ℂ) (embedding (mk (w.embedding.comp (algebraMap K L)))) (w.embedding.comp (algebraMap K L))
⊢ ¬Eq (α := ℂ) ((conjugate w.embedding : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ)
      ((w.embedding : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ)

Tactic:
aesop
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
x : K
hx :
  ¬Eq (α := ℂ) ((conjugate (embedding (mk (w.embedding.comp (algebraMap K L)))) : (a : K) → ℂ) x : ℂ)
      ((embedding (mk (w.embedding.comp (algebraMap K L))) : (a : K) → ℂ) x : ℂ)
h :
  Eq (α := K →+* ℂ) (embedding (mk (w.embedding.comp (algebraMap K L)))) (conjugate (w.embedding.comp (algebraMap K L)))
⊢ ¬Eq (α := ℂ) ((conjugate w.embedding : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ)
      ((w.embedding : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ)

Tactic:
aesop
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
hw : w.IsReal
rw : ∀ (hw : ¬w.IsComplex), ¬v.IsComplex
⊢ v.IsReal

Tactic:
rw [← not_isComplex_iff_isReal] at hw ⊢

Premises used: NumberField.InfinitePlace.not_isComplex_iff_isReal
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
hw : ¬w.IsComplex
⊢ ¬v.IsComplex

Tactic:
mt (isComplex_of_isComplex_under w) hw

Premises used: mt, NumberField.InfinitePlace.LiesOver.isComplex_of_isComplex_under
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
hw : ¬w.IsComplex
⊢ ¬v.IsComplex

Tactic:
exact mt (isComplex_of_isComplex_under w) hw

Premises used: mt, NumberField.InfinitePlace.LiesOver.isComplex_of_isComplex_under
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
hw : IsRamified K w
⊢ v.IsReal

Tactic:
LiesOver.comap_eq w v ▸ (isRamified_iff.1 hw).2

Premises used: Eq.rec, NumberField.InfinitePlace.LiesOver.comap_eq, NumberField.InfinitePlace.isRamified_iff, And.right, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
hw : IsUnramified K w
hv : v.IsReal
⊢ ¬IsComplex (w.comap (algebraMap K L))

Tactic:
simpa [LiesOver.comap_eq w v] using not_isComplex_iff_isReal.2 hv

Premises used: Iff.mpr, NumberField.InfinitePlace.not_isComplex_iff_isReal, NumberField.InfinitePlace.LiesOver.comap_eq
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
φ : L →+* ℂ
h : Membership.mem (γ := Set (L →+* ℂ)) (unmixedEmbeddingsOver L v.embedding) φ
⊢ Membership.mem (γ := Set (InfinitePlace L)) (unramifiedPlacesOver L v) (mk φ)

Tactic:
⟨⟨have := h.1; mk_embedding v ▸ LiesOver.comp_eq (mk φ).1 (mk v.embedding).1⟩,
    h.2.mk_isUnramified⟩

Premises used: AbsoluteValue.LiesOver.mk, Set.Mem, NumberField.InfinitePlace.unramifiedPlacesOver, NumberField.InfinitePlace.mk_embedding, setOf, Eq.rec, NumberField.InfinitePlace.mk, NumberField.InfinitePlace.embedding, AbsoluteValue.LiesOver.comp_eq, And.right, And.left, And.intro, Subtype.val, NumberField.ComplexEmbedding.IsUnmixed.mk_isUnramified
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
φ : L →+* ℂ
h : Membership.mem (γ := Set (L →+* ℂ)) (mixedEmbeddingsOver L v.embedding) φ
⊢ Membership.mem (γ := Set (InfinitePlace L)) (ramifiedPlacesOver L v) (mk φ)

Tactic:
⟨⟨have := h.1; mk_embedding v ▸ LiesOver.comp_eq (mk φ).1 (mk v.embedding).1⟩, h.2.mk_isRamified⟩

Premises used: NumberField.InfinitePlace.ramifiedPlacesOver, AbsoluteValue.LiesOver.mk, Set.Mem, NumberField.InfinitePlace.mk_embedding, setOf, Eq.rec, NumberField.InfinitePlace.mk, NumberField.InfinitePlace.embedding, NumberField.ComplexEmbedding.IsMixed.mk_isRamified, AbsoluteValue.LiesOver.comp_eq, And.right, And.left, And.intro, Subtype.val
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
hw : Membership.mem (γ := Set (InfinitePlace L)) (ramifiedPlacesOver L v) w
⊢ Membership.mem (γ := Set (L →+* ℂ)) (mixedEmbeddingsOver L v.embedding) w.embedding

Tactic:
⟨liesOver_embedding_of_mem_ramifiedPlacesOver hw, hw.2.isMixed_embedding⟩

Premises used: NumberField.ComplexEmbedding.mixedEmbeddingsOver, Set.Mem, setOf, NumberField.InfinitePlace.liesOver_embedding_of_mem_ramifiedPlacesOver, And.right, And.intro, NumberField.InfinitePlace.IsRamified.isMixed_embedding
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
hw : Membership.mem (γ := Set (InfinitePlace L)) (ramifiedPlacesOver L v) w
⊢ Membership.mem (γ := Set (L →+* ℂ)) (mixedEmbeddingsOver L v.embedding) (conjugate w.embedding)

Tactic:
⟨liesOver_conjugate_embedding_of_mem_ramifiedPlacesOver hw, hw.2.isMixed_conjugate_embedding⟩

Premises used: NumberField.ComplexEmbedding.mixedEmbeddingsOver, Set.Mem, NumberField.InfinitePlace.IsRamified.isMixed_conjugate_embedding, setOf, And.right, And.intro, NumberField.InfinitePlace.liesOver_conjugate_embedding_of_mem_ramifiedPlacesOver
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
⊢ Disjoint (α := Set (InfinitePlace L)) (ramifiedPlacesOver L v) (unramifiedPlacesOver L v)

Tactic:
grind [ramifiedPlacesOver, unramifiedPlacesOver]

Premises used: NumberField.InfinitePlace.ramifiedPlacesOver, NumberField.InfinitePlace.unramifiedPlacesOver
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
⊢ Eq.{u_5 + 1} (α := Set (InfinitePlace L))
    {a : InfinitePlace L |
      (↑a : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ) ∧ IsRamified K a ∨
        (↑a : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ) ∧ IsUnramified K a}
    {w : InfinitePlace L | (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)}

Tactic:
grind
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
ψ : L →+* ℂ
h : Membership.mem (γ := Set (L →+* ℂ)) (mixedEmbeddingsOver L v.embedding) ψ
hl : (mk ψ).embedding = ψ
⊢ Membership.mem (γ := Set (L →+* ℂ))
    (Sum.elim embedding (conjugate ∘ embedding) ''
      (OrderIso.symm Set.sumEquiv :
          (a : Set (InfinitePlace L) × Set (InfinitePlace L)) → Set (InfinitePlace L ⊕ InfinitePlace L))
        (ramifiedPlacesOver L v, ramifiedPlacesOver L v))
    ψ

Tactic:
simpa using .inl ⟨mk ψ, mk_mem_ramifiedPlacesOver h, hl⟩
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
ψ : L →+* ℂ
h : Membership.mem (γ := Set (L →+* ℂ)) (mixedEmbeddingsOver L v.embedding) ψ
hr : (mk ψ).embedding = conjugate ψ
⊢ conjugate (mk ψ).embedding = ψ

Tactic:
aesop
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
ψ : L →+* ℂ
h : Membership.mem (γ := Set (L →+* ℂ)) (mixedEmbeddingsOver L v.embedding) ψ
hr : (mk ψ).embedding = conjugate ψ
⊢ Membership.mem (γ := Set (L →+* ℂ))
    (Sum.elim embedding (conjugate ∘ embedding) ''
      (OrderIso.symm Set.sumEquiv :
          (a : Set (InfinitePlace L) × Set (InfinitePlace L)) → Set (InfinitePlace L ⊕ InfinitePlace L))
        (ramifiedPlacesOver L v, ramifiedPlacesOver L v))
    ψ

Tactic:
simpa using .inr ⟨mk ψ, mk_mem_ramifiedPlacesOver h, by aesop⟩
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
ψ : L →+* ℂ
h : Membership.mem (γ := Set (L →+* ℂ)) (mixedEmbeddingsOver L v.embedding) ψ
⊢ (mk ψ).embedding = ψ ∨ (mk ψ).embedding = conjugate ψ

Tactic:
cases embedding_mk_eq ψ with
        | inl hl => simpa using .inl ⟨mk ψ, mk_mem_ramifiedPlacesOver h, hl⟩
        | inr hr => simpa using .inr ⟨mk ψ, mk_mem_ramifiedPlacesOver h, by aesop⟩

Premises used: NumberField.InfinitePlace.embedding_mk_eq