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 : NumberField k
inst_4 : NumberField K
⊢ card.{u_1} (InfinitePlace k) ≤ card.{u_2} (InfinitePlace K)

Tactic:
have := Module.Finite.of_restrictScalars_finite ℚ k K
  Fintype.card_le_of_surjective _ comap_surjective

Premises used: Algebra.algebraMap, Rat, NumberField.InfinitePlace.comap, Module.Finite.of_restrictScalars_finite, NumberField.InfinitePlace.comap_surjective, Fintype.card_le_of_surjective
-- 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
σ : Gal(K/k)
w : InfinitePlace K
⊢ σ • w = w.comap (↑σ.symm : K →+* 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
inst_2 : Algebra k K
σ : Gal(K/k)
w : InfinitePlace K
x : K
⊢ Eq (α := ℝ) ((σ • w : (a : K) → ℝ) x : ℝ) ((w : (a : K) → ℝ) ((σ.symm : (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
inst_2 : Algebra k K
σ : Gal(K/k)
φ : K →+* ℂ
⊢ σ • mk φ = mk (φ.comp (↑σ.symm : K →+* K))

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_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
σ : Gal(K/k)
w : InfinitePlace K
f : F →+* K
⊢ (σ • w).comap f = w.comap (RingHom.comp (↑σ.symm : K →+* K) f)

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
inst_2 : Algebra k K
σ : Gal(K/k)
w : InfinitePlace K
⊢ (σ • w).IsReal ↔ w.IsReal

Tactic:
isReal_comap_iff (f := σ.symm.toRingEquiv)

Premises used: AlgEquiv.symm, MonoidHomClass.toMonoidHom, NumberField.InfinitePlace.isReal_comap_iff, RingHomClass.toRingHom, AlgEquiv.toRingEquiv
-- 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
σ : Gal(K/k)
w : InfinitePlace K
rw : ¬(σ • w).IsReal ↔ w.IsComplex
rw₁ : ¬(σ • w).IsReal ↔ ¬w.IsReal
rw₂ rw₃ : ¬w.IsReal ↔ ¬w.IsReal
⊢ (σ • w).IsComplex ↔ w.IsComplex

Tactic:
rw [← not_isReal_iff_isComplex, ← not_isReal_iff_isComplex, isReal_smul_iff]

Premises used: NumberField.InfinitePlace.isReal_smul_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
inst_3 : IsGalois k K
φ ψ : K →+* ℂ
h : Eq (α := k →+* ℂ) (φ.comp (algebraMap k K)) (ψ.comp (algebraMap k K))
⊢ ∃ (σ : Gal(K/k)), φ.comp (↑σ.symm : K →+* K) = ψ

Tactic:
NumberField.ComplexEmbedding.exists_comp_symm_eq_of_comp_eq φ ψ h

Premises used: NumberField.ComplexEmbedding.exists_comp_symm_eq_of_comp_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
inst_3 : IsGalois k K
w w' : InfinitePlace K
h : Eq (α := InfinitePlace k) (w.comap (algebraMap k K)) (w'.comap (algebraMap k K))
⊢ Eq (α := k →+* ℂ) (w.embedding.comp (algebraMap k K)) (w'.embedding.comp (algebraMap k K)) ∨
    Eq (α := k →+* ℂ) (conjugate (w.embedding.comp (algebraMap k K))) (w'.embedding.comp (algebraMap k K))

Tactic:
rw [← mk_embedding w, ← mk_embedding w', comap_mk, comap_mk, mk_eq_iff] at h

Premises used: NumberField.InfinitePlace.comap_mk, NumberField.InfinitePlace.mk_embedding, NumberField.InfinitePlace.mk_eq_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 : IsGalois k K
w w' : InfinitePlace K
h : Eq (α := k →+* ℂ) (w.embedding.comp (algebraMap k K)) (w'.embedding.comp (algebraMap k K))
inl : ∀ (σ : Gal(K/k)) (hσ : w.embedding.comp (↑σ.symm : K →+* K) = w'.embedding), ∃ (σ : Gal(K/k)), σ • w = w'
⊢ ∃ (σ : Gal(K/k)), σ • w = w'

Tactic:
obtain ⟨σ, hσ⟩ := ComplexEmbedding.exists_comp_symm_eq_of_comp_eq w.embedding w'.embedding h

Premises used: NumberField.InfinitePlace.ComplexEmbedding.exists_comp_symm_eq_of_comp_eq, NumberField.InfinitePlace.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
inst_3 : IsGalois k K
w w' : InfinitePlace K
h : Eq (α := k →+* ℂ) (w.embedding.comp (algebraMap k K)) (w'.embedding.comp (algebraMap k K))
σ : Gal(K/k)
hσ : w.embedding.comp (↑σ.symm : K →+* K) = w'.embedding
h₁ : σ • w = w'
⊢ ∃ (σ : Gal(K/k)), σ • w = w'

Tactic:
use σ
-- 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
w w' : InfinitePlace K
h : Eq (α := k →+* ℂ) (w.embedding.comp (algebraMap k K)) (w'.embedding.comp (algebraMap k K))
σ : Gal(K/k)
hσ : w.embedding.comp (↑σ.symm : K →+* K) = w'.embedding
h₁ : σ • mk w.embedding = w'
h₂ : σ • mk w.embedding = mk w'.embedding
h₃ : mk (w.embedding.comp (↑σ.symm : K →+* K)) = mk w'.embedding
h₄ h₅ : mk w'.embedding = mk w'.embedding
⊢ σ • w = w'

Tactic:
rw [← mk_embedding w, ← mk_embedding w', smul_mk, hσ]

Premises used: NumberField.InfinitePlace.mk_embedding, NumberField.InfinitePlace.smul_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
w w' : InfinitePlace K
h : Eq (α := k →+* ℂ) (conjugate (w.embedding.comp (algebraMap k K))) (w'.embedding.comp (algebraMap k K))
inr :
  ∀ (σ : Gal(K/k)) (hσ : (RingHom.comp (starRingEnd ℂ) w.embedding).comp (↑σ.symm : K →+* K) = w'.embedding),
    ∃ (σ : Gal(K/k)), σ • w = w'
⊢ ∃ (σ : Gal(K/k)), σ • w = w'

Tactic:
obtain ⟨σ, hσ⟩ := ComplexEmbedding.exists_comp_symm_eq_of_comp_eq
      ((starRingEnd ℂ).comp (embedding w)) w'.embedding h

Premises used: NumberField.InfinitePlace.ComplexEmbedding.exists_comp_symm_eq_of_comp_eq, NumberField.InfinitePlace.embedding, RingHom.comp, Complex, starRingEnd
-- 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
w w' : InfinitePlace K
h : Eq (α := k →+* ℂ) (conjugate (w.embedding.comp (algebraMap k K))) (w'.embedding.comp (algebraMap k K))
σ : Gal(K/k)
hσ : (RingHom.comp (starRingEnd ℂ) w.embedding).comp (↑σ.symm : K →+* K) = w'.embedding
h₁ : σ • w = w'
⊢ ∃ (σ : Gal(K/k)), σ • w = w'

Tactic:
use σ
-- 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
w w' : InfinitePlace K
h : Eq (α := k →+* ℂ) (conjugate (w.embedding.comp (algebraMap k K))) (w'.embedding.comp (algebraMap k K))
σ : Gal(K/k)
hσ : (RingHom.comp (starRingEnd ℂ) w.embedding).comp (↑σ.symm : K →+* K) = w'.embedding
h₁ :
  w.embedding.comp (↑σ.symm : K →+* K) = w'.embedding ∨ conjugate (w.embedding.comp (↑σ.symm : K →+* K)) = w'.embedding
⊢ σ • w = w'

Tactic:
rw [← mk_embedding w, ← mk_embedding w', smul_mk, mk_eq_iff]

Premises used: NumberField.InfinitePlace.mk_embedding, NumberField.InfinitePlace.smul_mk, NumberField.InfinitePlace.mk_eq_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 : IsGalois k K
w w' : InfinitePlace K
h : Eq (α := k →+* ℂ) (conjugate (w.embedding.comp (algebraMap k K))) (w'.embedding.comp (algebraMap k K))
σ : Gal(K/k)
hσ : (RingHom.comp (starRingEnd ℂ) w.embedding).comp (↑σ.symm : K →+* K) = w'.embedding
⊢ w.embedding.comp (↑σ.symm : K →+* K) = w'.embedding ∨ conjugate (w.embedding.comp (↑σ.symm : K →+* K)) = w'.embedding

Tactic:
Or.inr hσ

Premises used: Or.inr
-- 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
w w' : InfinitePlace K
h : Eq (α := k →+* ℂ) (conjugate (w.embedding.comp (algebraMap k K))) (w'.embedding.comp (algebraMap k K))
σ : Gal(K/k)
hσ : (RingHom.comp (starRingEnd ℂ) w.embedding).comp (↑σ.symm : K →+* K) = w'.embedding
⊢ w.embedding.comp (↑σ.symm : K →+* K) = w'.embedding ∨ conjugate (w.embedding.comp (↑σ.symm : K →+* K)) = w'.embedding

Tactic:
exact Or.inr hσ

Premises used: Or.inr
-- 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
w w' : InfinitePlace K
h :
  Eq (α := k →+* ℂ) (w.embedding.comp (algebraMap k K)) (w'.embedding.comp (algebraMap k K)) ∨
    Eq (α := k →+* ℂ) (conjugate (w.embedding.comp (algebraMap k K))) (w'.embedding.comp (algebraMap k K))
inl :
  ∀ (h : Eq (α := k →+* ℂ) (w.embedding.comp (algebraMap k K)) (w'.embedding.comp (algebraMap k K))),
    ∃ (σ : Gal(K/k)), σ • w = w'
inr :
  ∀ (h : Eq (α := k →+* ℂ) (conjugate (w.embedding.comp (algebraMap k K))) (w'.embedding.comp (algebraMap k K))),
    ∃ (σ : Gal(K/k)), σ • w = w'
⊢ ∃ (σ : Gal(K/k)), σ • w = w'

Tactic:
cases h with
  | inl h =>
    obtain ⟨σ, hσ⟩ := ComplexEmbedding.exists_comp_symm_eq_of_comp_eq w.embedding w'.embedding h
    use σ
    rw [← mk_embedding w, ← mk_embedding w', smul_mk, hσ]
  | inr h =>
    obtain ⟨σ, hσ⟩ := ComplexEmbedding.exists_comp_symm_eq_of_comp_eq
      ((starRingEnd ℂ).comp (embedding w)) w'.embedding h
    use σ
    rw [← mk_embedding w, ← mk_embedding w', smul_mk, mk_eq_iff]
    exact Or.inr hσ

Premises used: NumberField.InfinitePlace.mk_embedding, NumberField.InfinitePlace.smul_mk, NumberField.InfinitePlace.mk_eq_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 : IsGalois k K
w w' : InfinitePlace K
⊢ w' ∈ MulAction.orbit Gal(K/k) w ↔ Eq (α := InfinitePlace k) (w.comap (algebraMap k K)) (w'.comap (algebraMap k K))

Tactic:
⟨?_, exists_smul_eq_of_comap_eq⟩

Premises used: NumberField.InfinitePlace.exists_smul_eq_of_comap_eq, 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
inst_3 : IsGalois k K
w w' : InfinitePlace K
refine :
  w' ∈ MulAction.orbit Gal(K/k) w → Eq (α := InfinitePlace k) (w.comap (algebraMap k K)) (w'.comap (algebraMap k K))
⊢ w' ∈ MulAction.orbit Gal(K/k) w ↔ Eq (α := InfinitePlace k) (w.comap (algebraMap k K)) (w'.comap (algebraMap k K))

Tactic:
refine ⟨?_, exists_smul_eq_of_comap_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
inst_3 : IsGalois k K
w : InfinitePlace K
σ : Gal(K/k)
rw :
  Eq (α := InfinitePlace k) (mk (w.embedding.comp (algebraMap k K)))
    (mk (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (w.embedding.comp (↑σ.symm : K →+* K)) (algebraMap k K)))
⊢ Eq (α := InfinitePlace k) (w.comap (algebraMap k K)) ((σ • w).comap (algebraMap k K))

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

Premises used: NumberField.InfinitePlace.comap_mk, NumberField.InfinitePlace.mk_embedding, NumberField.InfinitePlace.smul_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
w : InfinitePlace K
σ : Gal(K/k)
e_φ :
  Eq (α := k →+* ℂ) (w.embedding.comp (algebraMap k K))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (w.embedding.comp (↑σ.symm : K →+* K)) (algebraMap k K))
⊢ Eq (α := InfinitePlace k) (mk (w.embedding.comp (algebraMap k K)))
    (mk (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (w.embedding.comp (↑σ.symm : K →+* K)) (algebraMap k K)))

Tactic:
congr 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
inst_3 : IsGalois k K
w : InfinitePlace K
σ : Gal(K/k)
e_φ :
  ∀ (x : k),
    Eq (α := ℂ) ((w.embedding.comp (algebraMap k K) : (a : k) → ℂ) x : ℂ)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (w.embedding.comp (↑σ.symm : K →+* K)) (algebraMap k K) :
            (a : k) → ℂ)
          x :
        ℂ)
⊢ Eq (α := k →+* ℂ) (w.embedding.comp (algebraMap k K))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (w.embedding.comp (↑σ.symm : K →+* K)) (algebraMap k K))

Tactic:
ext1
-- 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
w : InfinitePlace K
σ : Gal(K/k)
x : k
⊢ Eq (α := ℂ) ((w.embedding.comp (algebraMap k K) : (a : k) → ℂ) x : ℂ)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (w.embedding.comp (↑σ.symm : K →+* K)) (algebraMap k K) :
          (a : k) → ℂ)
        x :
      ℂ)

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 : Type u_3
inst_2 : Field F
inst_3 : Algebra k K
σ : Gal(K/k)
w : InfinitePlace K
inst_4 : IsGalois k K
refine_1 :
  Function.Injective.{u_2 + 1, u_1 + 1} (α :=
    Quotient (α := InfinitePlace K) (MulAction.orbitRel Gal(K/k) (InfinitePlace K))) (β := InfinitePlace k)
    (Quotient.lift (fun (x : InfinitePlace K) ↦ x.comap (algebraMap k K)) ⋯)
refine_2 :
  Function.Surjective.{u_2 + 1, u_1 + 1} (α :=
    Quotient (α := InfinitePlace K) (MulAction.orbitRel Gal(K/k) (InfinitePlace K))) (β := InfinitePlace k)
    (Quotient.lift (fun (x : InfinitePlace K) ↦ x.comap (algebraMap k K)) ⋯)
⊢ Equiv.{u_2 + 1, u_1 + 1} (Quotient (α := InfinitePlace K) (MulAction.orbitRel Gal(K/k) (InfinitePlace K)))
    (InfinitePlace k)

Tactic:
refine Equiv.ofBijective (Quotient.lift (comap · (algebraMap k K))
    fun _ _ e ↦ (mem_orbit_iff.mp e).symm) ⟨?_, ?_⟩

Premises used: Algebra.algebraMap, NumberField.InfinitePlace.comap, And.intro, Equiv.ofBijective, Iff.mp, Quotient.lift, NumberField.InfinitePlace.mem_orbit_iff, Eq.symm
-- 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
σ : Gal(K/k)
w_1 : InfinitePlace K
inst_4 : IsGalois k K
a₁ : Quotient (α := InfinitePlace K) (MulAction.orbitRel Gal(K/k) (InfinitePlace K))
w : InfinitePlace K
a₂ : Quotient (α := InfinitePlace K) (MulAction.orbitRel Gal(K/k) (InfinitePlace K))
w' : InfinitePlace K
e :
  Eq.{u_1 + 1} (α := InfinitePlace k)
    (Quotient.lift (s := MulAction.orbitRel Gal(K/k) (InfinitePlace K))
      (fun (x : InfinitePlace K) ↦ x.comap (algebraMap k K)) ⋯
      (Quot.mk (⇑(MulAction.orbitRel Gal(K/k) (InfinitePlace K)) : InfinitePlace K → InfinitePlace K → Prop) w))
    (Quotient.lift (s := MulAction.orbitRel Gal(K/k) (InfinitePlace K))
      (fun (x : InfinitePlace K) ↦ x.comap (algebraMap k K)) ⋯
      (Quot.mk (⇑(MulAction.orbitRel Gal(K/k) (InfinitePlace K)) : InfinitePlace K → InfinitePlace K → Prop) w'))
⊢ Eq (α := Quotient (α := InfinitePlace K) (MulAction.orbitRel Gal(K/k) (InfinitePlace K)))
    (Quot.mk (⇑(MulAction.orbitRel Gal(K/k) (InfinitePlace K)) : InfinitePlace K → InfinitePlace K → Prop) w)
    (Quot.mk (⇑(MulAction.orbitRel Gal(K/k) (InfinitePlace K)) : InfinitePlace K → InfinitePlace K → Prop) w')

Tactic:
Quotient.sound (mem_orbit_iff.mpr e.symm)

Premises used: Iff.mpr, NumberField.InfinitePlace.mem_orbit_iff, Quotient.sound, Eq.symm
-- 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
σ : Gal(K/k)
w_1 : InfinitePlace K
inst_4 : IsGalois k K
a₁ : Quotient (α := InfinitePlace K) (MulAction.orbitRel Gal(K/k) (InfinitePlace K))
w : InfinitePlace K
a₂ : Quotient (α := InfinitePlace K) (MulAction.orbitRel Gal(K/k) (InfinitePlace K))
w' : InfinitePlace K
e :
  Eq.{u_1 + 1} (α := InfinitePlace k)
    (Quotient.lift (s := MulAction.orbitRel Gal(K/k) (InfinitePlace K))
      (fun (x : InfinitePlace K) ↦ x.comap (algebraMap k K)) ⋯
      (Quot.mk (⇑(MulAction.orbitRel Gal(K/k) (InfinitePlace K)) : InfinitePlace K → InfinitePlace K → Prop) w))
    (Quotient.lift (s := MulAction.orbitRel Gal(K/k) (InfinitePlace K))
      (fun (x : InfinitePlace K) ↦ x.comap (algebraMap k K)) ⋯
      (Quot.mk (⇑(MulAction.orbitRel Gal(K/k) (InfinitePlace K)) : InfinitePlace K → InfinitePlace K → Prop) w'))
⊢ Eq (α := Quotient (α := InfinitePlace K) (MulAction.orbitRel Gal(K/k) (InfinitePlace K)))
    (Quot.mk (⇑(MulAction.orbitRel Gal(K/k) (InfinitePlace K)) : InfinitePlace K → InfinitePlace K → Prop) w)
    (Quot.mk (⇑(MulAction.orbitRel Gal(K/k) (InfinitePlace K)) : InfinitePlace K → InfinitePlace K → Prop) w')

Tactic:
exact Quotient.sound (mem_orbit_iff.mpr e.symm)

Premises used: Quotient.sound
-- 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
σ : Gal(K/k)
w_1 : InfinitePlace K
inst_4 : IsGalois k K
w : InfinitePlace k
refine_2 :
  ∀ (w' : InfinitePlace K) (hw : (fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w' = w),
    ∃ (a : Quotient (α := InfinitePlace K) (MulAction.orbitRel Gal(K/k) (InfinitePlace K))),
      Quotient.lift (fun (x : InfinitePlace K) ↦ x.comap (algebraMap k K)) ⋯ a = w
⊢ ∃ (a : Quotient (α := InfinitePlace K) (MulAction.orbitRel Gal(K/k) (InfinitePlace K))),
    Quotient.lift (fun (x : InfinitePlace K) ↦ x.comap (algebraMap k K)) ⋯ a = w

Tactic:
obtain ⟨w', hw⟩ := comap_surjective (K := K) w

Premises used: NumberField.InfinitePlace.comap_surjective
-- 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
σ : Gal(K/k)
w_1 : InfinitePlace K
inst_4 : IsGalois k K
w : InfinitePlace k
w' : InfinitePlace K
hw : (fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w' = w
⊢ ∃ (a : Quotient (α := InfinitePlace K) (MulAction.orbitRel Gal(K/k) (InfinitePlace K))),
    Quotient.lift (fun (x : InfinitePlace K) ↦ x.comap (algebraMap k K)) ⋯ a = w

Tactic:
⟨⟦w'⟧, hw⟩

Premises used: Quotient.mk, Exists.intro
-- 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
σ : Gal(K/k)
w_1 : InfinitePlace K
inst_4 : IsGalois k K
w : InfinitePlace k
w' : InfinitePlace K
hw : (fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w' = w
⊢ ∃ (a : Quotient (α := InfinitePlace K) (MulAction.orbitRel Gal(K/k) (InfinitePlace K))),
    Quotient.lift (fun (x : InfinitePlace K) ↦ x.comap (algebraMap k K)) ⋯ a = w

Tactic:
exact ⟨⟦w'⟧, hw⟩
-- 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
w : InfinitePlace K
⊢ Eq.{u_1 + 1} (α := InfinitePlace k)
    ((orbitRelEquiv : (a : Quotient (MulAction.orbitRel Gal(K/k) (InfinitePlace K))) → InfinitePlace k)
        (Quotient.mk'' w) :
      InfinitePlace k)
    (w.comap (algebraMap k K) : InfinitePlace k)

Tactic:
rfl

Premises used: NumberField.InfinitePlace.comap, rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Goal:
K : Type u_2
inst : Field K
w : InfinitePlace K
⊢ IsUnramified K w

Tactic:
rfl

Premises used: NumberField.InfinitePlace.comap, NumberField.InfinitePlace.IsUnramified, 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
inst_2 : Algebra k K
w : InfinitePlace K
h : IsUnramified k w
⊢ mult (w.comap (algebraMap k K)) = w.mult

Tactic:
h

Premises used: NumberField.InfinitePlace.IsUnramified
-- 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 : mult (w.comap (algebraMap k K)) ≤ w.mult
⊢ IsUnramified k w ↔ w.mult ≤ mult (w.comap (algebraMap k K))

Tactic:
rw [IsUnramified, le_antisymm_iff, and_iff_right]

Premises used: and_iff_right, NumberField.InfinitePlace.IsUnramified, le_antisymm_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
⊢ mult (w.comap (algebraMap k K)) ≤ w.mult

Tactic:
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
inst_2 : Algebra k K
w : InfinitePlace K
⊢ mult (w.comap (algebraMap k K)) ≤ w.mult

Tactic:
exact 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
w : InfinitePlace F
h : IsUnramified k w
f : K →ₐ[k] F
rw : mult (w.comap (↑f : K →+* F)) ≤ w.mult
⊢ IsUnramified k (w.comap (↑f : K →+* F))

Tactic:
rw [InfinitePlace.isUnramified_iff_mult_le, ← InfinitePlace.comap_comp, f.comp_algebraMap, h.eq]

Premises used: AlgHom.comp_algebraMap, NumberField.InfinitePlace.comap_comp, NumberField.InfinitePlace.IsUnramified.eq, NumberField.InfinitePlace.isUnramified_iff_mult_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
w : InfinitePlace F
h : IsUnramified k w
f : K →ₐ[k] F
⊢ mult (w.comap (↑f : K →+* F)) ≤ w.mult

Tactic:
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
w : InfinitePlace F
h : IsUnramified k w
f : K →ₐ[k] F
⊢ mult (w.comap (↑f : K →+* F)) ≤ w.mult

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
rw : mult (comap (w.comap (algebraMap K F)) (algebraMap k K)) ≤ mult (w.comap (algebraMap K F))
⊢ IsUnramified K w

Tactic:
rw [InfinitePlace.isUnramified_iff_mult_le, ← h.eq, IsScalarTower.algebraMap_eq k K F,
    InfinitePlace.comap_comp]

Premises used: NumberField.InfinitePlace.comap_comp, NumberField.InfinitePlace.IsUnramified.eq, IsScalarTower.algebraMap_eq, NumberField.InfinitePlace.isUnramified_iff_mult_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
⊢ mult (comap (w.comap (algebraMap K F)) (algebraMap k K)) ≤ mult (w.comap (algebraMap K F))

Tactic:
InfinitePlace.mult_comap_le _ _

Premises used: NumberField.InfinitePlace.mult_comap_le