awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
h : IsRamified K w
H : w.IsComplex ∧ v.IsReal
this : ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)
rw : Module.finrank ℝ ℂ = 2
rw₁ rw₂ : Eq (α := ℕ) 2 2
⊢ Module.finrank.{u_1, u_2} v.Completion w.Completion = 2

Tactic:
rw [Algebra.finrank_eq_of_equiv_equiv (ringEquivRealOfIsReal H.2)
      (ringEquivComplexOfIsComplex H.1) (by ext; simp),
    Complex.finrank_real_complex]

Premises used: NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal, Algebra.finrank_eq_of_equiv_equiv, And.right, And.left, NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex, Complex.finrank_real_complex
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
h : IsUnramified K w
inl : ∀ (hv : v.IsReal), Module.finrank.{u_1, u_2} v.Completion w.Completion = 1
inr : ∀ (hv : v.IsComplex), Module.finrank.{u_1, u_2} v.Completion w.Completion = 1
⊢ Module.finrank.{u_1, u_2} v.Completion w.Completion = 1

Tactic:
rcases v.isReal_or_isComplex with (hv | hv)

Premises used: NumberField.InfinitePlace.isReal_or_isComplex
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
h : IsUnramified K w
hv : v.IsReal
⊢ ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)

Tactic:
have := LiesOver.extensionEmbedding_liesOver_of_isReal w hv
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
h : IsUnramified K w
hv : v.IsReal
this : ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)
x : v.Completion
⊢ (↑((RingHom.comp (algebraMap ℝ ℝ) (ringEquivRealOfIsReal hv).toRingHom : (a : v.Completion) → ℝ) x) : ℂ) =
    (↑(((ringEquivRealOfIsReal ⋯).toRingHom.comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℝ) x) :
      ℂ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
h : IsUnramified K w
hv : v.IsReal
this : ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)
inl : Module.finrank ℝ ℝ = 1
inl₁ inl₂ : Eq (α := ℕ) 1 1
⊢ Module.finrank.{u_1, u_2} v.Completion w.Completion = 1

Tactic:
rw [Algebra.finrank_eq_of_equiv_equiv (ringEquivRealOfIsReal hv) (ringEquivRealOfIsReal
        (h.liesOver_isReal_over _ _ hv)) (RingHom.ext fun _ ↦ Complex.ofReal_inj.1 <| by simp),
      Module.finrank_self]

Premises used: NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal, Algebra.finrank_eq_of_equiv_equiv, RingHom.ext, Iff.mp, Complex.ofReal_inj, Module.finrank_self, NumberField.InfinitePlace.IsUnramified.liesOver_isReal_over
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
h : IsUnramified K w
hv : v.IsComplex
hl : w.embedding.comp (algebraMap K L) = v.embedding
⊢ ComplexEmbedding.LiesOver w.embedding v.embedding

Tactic:
have : ComplexEmbedding.LiesOver w.embedding v.embedding := ⟨hl⟩
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
h : IsUnramified K w
hv : v.IsComplex
hl : w.embedding.comp (algebraMap K L) = v.embedding
this : ComplexEmbedding.LiesOver w.embedding v.embedding
⊢ ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)

Tactic:
have := liesOver_extensionEmbedding w v
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
h : IsUnramified K w
hv : v.IsComplex
hl : w.embedding.comp (algebraMap K L) = v.embedding
this_1 : ComplexEmbedding.LiesOver w.embedding v.embedding
this : ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)
a :
  ∀ (x : v.Completion),
    Eq (α := ℂ)
      ((RingHom.comp (algebraMap ℂ ℂ) (ringEquivComplexOfIsComplex hv).toRingHom : (a : v.Completion) → ℂ) x : ℂ)
      (((ringEquivComplexOfIsComplex ⋯).toRingHom.comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ)
          x :
        ℂ)
⊢ RingHom.comp (algebraMap ℂ ℂ) (ringEquivComplexOfIsComplex hv).toRingHom =
    (ringEquivComplexOfIsComplex ⋯).toRingHom.comp (algebraMap v.Completion w.Completion)

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
h : IsUnramified K w
hv : v.IsComplex
hl : w.embedding.comp (algebraMap K L) = v.embedding
this_1 : ComplexEmbedding.LiesOver w.embedding v.embedding
this : ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)
x : v.Completion
⊢ Eq (α := ℂ)
    ((RingHom.comp (algebraMap ℂ ℂ) (ringEquivComplexOfIsComplex hv).toRingHom : (a : v.Completion) → ℂ) x : ℂ)
    (((ringEquivComplexOfIsComplex ⋯).toRingHom.comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ)
        x :
      ℂ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
h : IsUnramified K w
hv : v.IsComplex
hl : w.embedding.comp (algebraMap K L) = v.embedding
this_1 : ComplexEmbedding.LiesOver w.embedding v.embedding
this : ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)
inr : Module.finrank ℂ ℂ = 1
inr₁ inr₂ : Eq (α := ℕ) 1 1
⊢ Module.finrank.{u_1, u_2} v.Completion w.Completion = 1

Tactic:
rw [Algebra.finrank_eq_of_equiv_equiv (ringEquivComplexOfIsComplex hv)
          (ringEquivComplexOfIsComplex (LiesOver.isComplex_of_isComplex_under _ hv)) (by ext; simp),
        Module.finrank_self]

Premises used: Algebra.finrank_eq_of_equiv_equiv, NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex, Module.finrank_self
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
h : IsUnramified K w
hv : v.IsComplex
hr : (conjugate w.embedding).comp (algebraMap K L) = v.embedding
⊢ ComplexEmbedding.LiesOver (conjugate w.embedding) v.embedding

Tactic:
have : ComplexEmbedding.LiesOver (conjugate w.embedding) v.embedding := ⟨hr⟩
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
h : IsUnramified K w
hv : v.IsComplex
hr : (conjugate w.embedding).comp (algebraMap K L) = v.embedding
this : ComplexEmbedding.LiesOver (conjugate w.embedding) v.embedding
⊢ ComplexEmbedding.LiesOver (conjugate (extensionEmbedding w)) (extensionEmbedding v)

Tactic:
have := liesOver_conjugate_extensionEmbedding w v
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
h : IsUnramified K w
hv : v.IsComplex
hr : (conjugate w.embedding).comp (algebraMap K L) = v.embedding
this_1 : ComplexEmbedding.LiesOver (conjugate w.embedding) v.embedding
this : ComplexEmbedding.LiesOver (conjugate (extensionEmbedding w)) (extensionEmbedding v)
a :
  ∀ (x : v.Completion),
    Eq (α := ℂ)
      ((RingHom.comp (algebraMap ℂ ℂ) (ringEquivComplexOfIsComplex hv).toRingHom : (a : v.Completion) → ℂ) x : ℂ)
      ((((ringEquivComplexOfIsComplex ⋯).trans starRingAut).toRingHom.comp (algebraMap v.Completion w.Completion) :
            (a : v.Completion) → ℂ)
          x :
        ℂ)
⊢ RingHom.comp (algebraMap ℂ ℂ) (ringEquivComplexOfIsComplex hv).toRingHom =
    ((ringEquivComplexOfIsComplex ⋯).trans starRingAut).toRingHom.comp (algebraMap v.Completion w.Completion)

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
h : IsUnramified K w
hv : v.IsComplex
hr : (conjugate w.embedding).comp (algebraMap K L) = v.embedding
this_1 : ComplexEmbedding.LiesOver (conjugate w.embedding) v.embedding
this : ComplexEmbedding.LiesOver (conjugate (extensionEmbedding w)) (extensionEmbedding v)
x : v.Completion
⊢ Eq (α := ℂ)
    ((RingHom.comp (algebraMap ℂ ℂ) (ringEquivComplexOfIsComplex hv).toRingHom : (a : v.Completion) → ℂ) x : ℂ)
    ((((ringEquivComplexOfIsComplex ⋯).trans starRingAut).toRingHom.comp (algebraMap v.Completion w.Completion) :
          (a : v.Completion) → ℂ)
        x :
      ℂ)

Tactic:
simp [← conjugate_coe_eq]

Premises used: NumberField.ComplexEmbedding.conjugate_coe_eq
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
h : IsUnramified K w
hv : v.IsComplex
hr : (conjugate w.embedding).comp (algebraMap K L) = v.embedding
this_1 : ComplexEmbedding.LiesOver (conjugate w.embedding) v.embedding
this : ComplexEmbedding.LiesOver (conjugate (extensionEmbedding w)) (extensionEmbedding v)
inr : Module.finrank ℂ ℂ = 1
inr₁ inr₂ : Eq (α := ℕ) 1 1
⊢ Module.finrank.{u_1, u_2} v.Completion w.Completion = 1

Tactic:
rw [Algebra.finrank_eq_of_equiv_equiv (ringEquivComplexOfIsComplex hv)
        ((ringEquivComplexOfIsComplex (LiesOver.isComplex_of_isComplex_under _ hv)).trans
          (starRingAut (R := ℂ))) (by ext; simp [← conjugate_coe_eq]),
        Module.finrank_self]

Premises used: Algebra.finrank_eq_of_equiv_equiv, NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex, Module.finrank_self
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
h : IsUnramified K w
hv : v.IsComplex
⊢ w.embedding.comp (algebraMap K L) = v.embedding ∨ (conjugate w.embedding).comp (algebraMap K L) = v.embedding

Tactic:
cases LiesOver.embedding_comp_eq_or_conjugate_embedding_comp_eq w v with
    | inl hl =>
      have : ComplexEmbedding.LiesOver w.embedding v.embedding := ⟨hl⟩
      have := liesOver_extensionEmbedding w v
      rw [Algebra.finrank_eq_of_equiv_equiv (ringEquivComplexOfIsComplex hv)
          (ringEquivComplexOfIsComplex (LiesOver.isComplex_of_isComplex_under _ hv)) (by ext; simp),
        Module.finrank_self]
    | inr hr =>
      have : ComplexEmbedding.LiesOver (conjugate w.embedding) v.embedding := ⟨hr⟩
      have := liesOver_conjugate_extensionEmbedding w v
      rw [Algebra.finrank_eq_of_equiv_equiv (ringEquivComplexOfIsComplex hv)
        ((ringEquivComplexOfIsComplex (LiesOver.isComplex_of_isComplex_under _ hv)).trans
          (starRingAut (R := ℂ))) (by ext; simp [← conjugate_coe_eq]),
        Module.finrank_self]

Premises used: NumberField.InfinitePlace.LiesOver.embedding_comp_eq_or_conjugate_embedding_comp_eq, Algebra.finrank_eq_of_equiv_equiv, NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex, Module.finrank_self
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
⊢ v.inertiaDeg w = Ideal.inertiaDeg.{u_1, u_2} (R := v.Completion) (S := w.Completion) ⊥ ⊥

Tactic:
simp only [InfinitePlace.inertiaDeg, dif_pos]

Premises used: dif_pos, NumberField.InfinitePlace.inertiaDeg
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
simp :
  (if h : True then
      Module.finrank.{u_1, u_2} (HasQuotient.Quotient v.Completion (B := Ideal v.Completion) ⊥)
        (HasQuotient.Quotient w.Completion (B := Ideal w.Completion) ⊥)
    else 0) =
    Module.finrank.{u_1, u_2} v.Completion w.Completion
⊢ v.inertiaDeg w = Module.finrank.{u_1, u_2} v.Completion w.Completion

Tactic:
simp only [inertiaDeg_of_liesOver, Ideal.inertiaDeg, Ideal.comap_bot_of_injective _ <|
    FaithfulSMul.algebraMap_injective v.Completion w.Completion]

Premises used: Ideal.inertiaDeg, NumberField.InfinitePlace.Completion, Ideal.comap_bot_of_injective, FaithfulSMul.algebraMap_injective, NumberField.InfinitePlace.inertiaDeg_of_liesOver
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
h :
  ∀ (x : v.Completion),
    Eq.{u_2 + 1} (α := w.Completion)
      ((@RingHom.comp _ (HasQuotient.Quotient v.Completion (B := Ideal v.Completion) ⊥) _ _ Semiring.toNonAssocSemiring
              _
              (RingHom.comp (algebraMap v.Completion w.Completion)
                (RingEquiv.toRingHom (RingEquiv.quotientBot v.Completion)))
              (Ideal.Quotient.mk ⊥) :
            (a : v.Completion) → w.Completion)
          x :
        w.Completion)
      ((RingHom.comp (β := HasQuotient.Quotient v.Completion (B := Ideal v.Completion) ⊥)
              (RingHom.comp (RingEquiv.toRingHom (RingEquiv.quotientBot w.Completion))
                (algebraMap (HasQuotient.Quotient v.Completion (B := Ideal v.Completion) ⊥)
                  (HasQuotient.Quotient w.Completion (B := Ideal w.Completion) ⊥)))
              (Ideal.Quotient.mk ⊥) :
            (a : v.Completion) → w.Completion)
          x :
        w.Completion)
⊢ Eq (α := RingHom.{u_1, u_2} (HasQuotient.Quotient v.Completion (B := Ideal v.Completion) ⊥) w.Completion)
    (RingHom.comp (algebraMap v.Completion w.Completion) (RingEquiv.toRingHom (RingEquiv.quotientBot v.Completion)))
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.quotientBot w.Completion))
      (algebraMap (HasQuotient.Quotient v.Completion (B := Ideal v.Completion) ⊥)
        (HasQuotient.Quotient w.Completion (B := Ideal w.Completion) ⊥)))

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
x : v.Completion
⊢ Eq.{u_2 + 1} (α := w.Completion)
    ((@RingHom.comp _ (HasQuotient.Quotient v.Completion (B := Ideal v.Completion) ⊥) _ _ Semiring.toNonAssocSemiring _
            (RingHom.comp (algebraMap v.Completion w.Completion)
              (RingEquiv.toRingHom (RingEquiv.quotientBot v.Completion)))
            (Ideal.Quotient.mk ⊥) :
          (a : v.Completion) → w.Completion)
        x :
      w.Completion)
    ((RingHom.comp (β := HasQuotient.Quotient v.Completion (B := Ideal v.Completion) ⊥)
            (RingHom.comp (RingEquiv.toRingHom (RingEquiv.quotientBot w.Completion))
              (algebraMap (HasQuotient.Quotient v.Completion (B := Ideal v.Completion) ⊥)
                (HasQuotient.Quotient w.Completion (B := Ideal w.Completion) ⊥)))
            (Ideal.Quotient.mk ⊥) :
          (a : v.Completion) → w.Completion)
        x :
      w.Completion)

Tactic:
simp [RingHom.algebraMap_toAlgebra]

Premises used: RingHom.algebraMap_toAlgebra
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
⊢ (if h : True then
      Module.finrank.{u_1, u_2} (HasQuotient.Quotient v.Completion (B := Ideal v.Completion) ⊥)
        (HasQuotient.Quotient w.Completion (B := Ideal w.Completion) ⊥)
    else 0) =
    Module.finrank.{u_1, u_2} v.Completion w.Completion

Tactic:
exact Algebra.finrank_eq_of_equiv_equiv (RingEquiv.quotientBot v.Completion)
    (RingEquiv.quotientBot w.Completion) (by ext; simp [RingHom.algebraMap_toAlgebra])

Premises used: NumberField.InfinitePlace.Completion, Algebra.finrank_eq_of_equiv_equiv, RingEquiv.quotientBot
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
hw : Membership.mem (γ := Set (InfinitePlace L)) (unramifiedPlacesOver L v) w
⊢ v.inertiaDeg w = 1

Tactic:
have := (Set.mem_setOf.1 hw).1; finrank_eq_one_of_isUnramified v hw.2 ▸ inertiaDeg_eq_finrank v w

Premises used: Eq.rec, Set.mem_setOf, NumberField.InfinitePlace.Completion.finrank_eq_one_of_isUnramified, NumberField.InfinitePlace.inertiaDeg_eq_finrank, And.right, And.left, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
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
⊢ v.inertiaDeg w = 2

Tactic:
have := (Set.mem_setOf.1 hw).1; finrank_eq_two_of_isRamified v hw.2 ▸ inertiaDeg_eq_finrank v w

Premises used: Eq.rec, Set.mem_setOf, NumberField.InfinitePlace.inertiaDeg_eq_finrank, And.right, And.left, NumberField.InfinitePlace.Completion.finrank_eq_two_of_isRamified, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
inst_3 : NumberField K
inst_4 : NumberField L
x : InfinitePlace L
h : Membership.mem (γ := Finset (InfinitePlace L)) (toFinset (ramifiedPlacesOver L v)) x
⊢ Membership.mem (γ := Set (InfinitePlace L)) (ramifiedPlacesOver L v) x

Tactic:
simpa using h
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
inst_3 : NumberField K
inst_4 : NumberField L
x : InfinitePlace L
h : Membership.mem (γ := Finset (InfinitePlace L)) (toFinset (unramifiedPlacesOver L v)) x
⊢ Membership.mem (γ := Set (InfinitePlace L)) (unramifiedPlacesOver L v) x

Tactic:
simpa using h
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
inst_3 : NumberField K
inst_4 : NumberField L
rw :
  ∑ x ∈ toFinset (unramifiedPlacesOver L v), 1 +
      HSMul.hSMul (β := ℕ) (card (α := InfinitePlace L) (toFinset (ramifiedPlacesOver L v))) 2 =
    Module.finrank K L
⊢ ∑ w ∈ toFinset (placesOver L v), v.inertiaDeg w = Module.finrank K L

Tactic:
rw [← union_ramifiedPlacesOver_unramifiedPlacesOver L v, toFinset_union,
    sum_union (Set.disjoint_toFinset.2 <| disjoint_ramifiedPlacesOver_unramifiedPlacesOver L v),
    sum_congr rfl (fun _ h ↦ inertiaDeg_eq_two (by simpa using h)),
    sum_congr rfl (fun _ h ↦ inertiaDeg_eq_one (by simpa using h)), sum_const, add_comm]

Premises used: Iff.mpr, Set.toFinset_union, NumberField.InfinitePlace.inertiaDeg_eq_one, Set.disjoint_toFinset, Finset.sum_union, add_comm, NumberField.InfinitePlace.inertiaDeg_eq_two, NumberField.InfinitePlace.union_ramifiedPlacesOver_unramifiedPlacesOver, NumberField.InfinitePlace.disjoint_ramifiedPlacesOver_unramifiedPlacesOver, Finset.sum_congr, rfl, Finset.sum_const
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
inst_3 : NumberField K
inst_4 : NumberField L
⊢ ∑ x ∈ toFinset (unramifiedPlacesOver L v), 1 +
      HSMul.hSMul (β := ℕ) (card (α := InfinitePlace L) (toFinset (ramifiedPlacesOver L v))) 2 =
    Module.finrank K L

Tactic:
simp [← unramifedPlacesOver_ncard_add_eq_finrank L v, mul_comm, ncard_eq_toFinset_card']

Premises used: Set.ncard_eq_toFinset_card', mul_comm, NumberField.InfinitePlace.unramifedPlacesOver_ncard_add_eq_finrank
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
k : ℕ
K : Type u
inst : Field K
inst_1 : CharZero K
inst_2 : NeZero k
inst_3 : IsCyclotomicExtension {k} ℚ K
⊢ Module.finrank ℚ K = φ k

Tactic:
IsCyclotomicExtension.finrank K <| Polynomial.cyclotomic.irreducible_rat (NeZero.pos _)

Premises used: IsCyclotomicExtension.finrank, Polynomial.cyclotomic.irreducible_rat, NeZero.pos
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hk : p ^ (k + 1) ≠ 2
rw :
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K)
⊢ Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    HPow.hPow (α := ℚ) (-1) (φ (p ^ (k + 1)) / 2) * HPow.hPow (α := ℚ) (↑p : ℚ) (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
rw [← discr_prime_pow_ne_two hζ (cyclotomic.irreducible_rat (NeZero.pos _)) hk]

Premises used: IsCyclotomicExtension.discr_prime_pow_ne_two, Polynomial.cyclotomic.irreducible_rat, NeZero.pos
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hk : p ^ (k + 1) ≠ 2
⊢ Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K)

Tactic:
hζ.discr_zeta_eq_discr_zeta_sub_one.symm

Premises used: IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one, Eq.symm