awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.InfinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : Algebra.{u_1, u_2} v.Completion w.Completion
inst_4 : IsScalarTower.{u_1, u_1, u_2} K v.Completion w.Completion
inst_5 : ContinuousSMul.{u_1, u_2} v.Completion w.Completion
inst_6 : ComplexEmbedding.LiesOver w.embedding v.embedding
x : v.Completion
⊢ Eq (α := ℂ) (((extensionEmbedding w).comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ) x : ℂ)
    ((extensionEmbedding v : (a : v.Completion) → ℂ) x : ℂ)
have a : IsClosed.{u_1} (X := UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ)))
  {a : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ)) |
    Eq (α := ℂ) (((extensionEmbedding w).comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ) a : ℂ)
      ((extensionEmbedding v : (a : v.Completion) → ℂ) a : ℂ)}
Tactic: induction x using induction_on
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.InfinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : Algebra.{u_1, u_2} v.Completion w.Completion
inst_4 : IsScalarTower.{u_1, u_1, u_2} K v.Completion w.Completion
inst_5 : ContinuousSMul.{u_1, u_2} v.Completion w.Completion
inst_6 : ComplexEmbedding.LiesOver w.embedding v.embedding
x : v.Completion
a :
  IsClosed.{u_1} (X := UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ)))
    {a : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ)) |
      Eq (α := ℂ) (((extensionEmbedding w).comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ) a : ℂ)
        ((extensionEmbedding v : (a : v.Completion) → ℂ) a : ℂ)}
⊢ Eq (α := ℂ) (((extensionEmbedding w).comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ) x : ℂ)
    ((extensionEmbedding v : (a : v.Completion) → ℂ) x : ℂ)
have a₁ : ∀ (a : WithAbs (↑v : AbsoluteValue K ℝ)),
  Eq (α := ℂ)
    (((extensionEmbedding w).comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ)
        (↑a : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ))) :
      ℂ)
    ((extensionEmbedding v : (a : v.Completion) → ℂ) (↑a : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ))) :
      ℂ)
Tactic: induction x using induction_on
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.InfinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : Algebra.{u_1, u_2} v.Completion w.Completion
inst_4 : IsScalarTower.{u_1, u_1, u_2} K v.Completion w.Completion
inst_5 : ContinuousSMul.{u_1, u_2} v.Completion w.Completion
inst_6 : ComplexEmbedding.LiesOver (conjugate w.embedding) v.embedding
⊢ (conjugate (extensionEmbedding w)).comp (algebraMap v.Completion w.Completion) = extensionEmbedding v
have a : ∀ (x : v.Completion),
  Eq (α := ℂ)
    (((conjugate (extensionEmbedding w)).comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ) x : ℂ)
    ((extensionEmbedding v : (a : v.Completion) → ℂ) x : ℂ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.InfinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : Algebra.{u_1, u_2} v.Completion w.Completion
inst_4 : IsScalarTower.{u_1, u_1, u_2} K v.Completion w.Completion
inst_5 : ContinuousSMul.{u_1, u_2} v.Completion w.Completion
inst_6 : ComplexEmbedding.LiesOver (conjugate w.embedding) v.embedding
x : v.Completion
⊢ Eq (α := ℂ)
    (((conjugate (extensionEmbedding w)).comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ) x : ℂ)
    ((extensionEmbedding v : (a : v.Completion) → ℂ) x : ℂ)
have a : IsClosed.{u_1} (X := UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ)))
  {a : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ)) |
    Eq (α := ℂ)
      (((conjugate (extensionEmbedding w)).comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ) a : ℂ)
      ((extensionEmbedding v : (a : v.Completion) → ℂ) a : ℂ)}
Tactic: induction x using induction_on
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.InfinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : Algebra.{u_1, u_2} v.Completion w.Completion
inst_4 : IsScalarTower.{u_1, u_1, u_2} K v.Completion w.Completion
inst_5 : ContinuousSMul.{u_1, u_2} v.Completion w.Completion
inst_6 : ComplexEmbedding.LiesOver (conjugate w.embedding) v.embedding
x : v.Completion
a :
  IsClosed.{u_1} (X := UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ)))
    {a : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ)) |
      Eq (α := ℂ)
        (((conjugate (extensionEmbedding w)).comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ) a :
          ℂ)
        ((extensionEmbedding v : (a : v.Completion) → ℂ) a : ℂ)}
⊢ Eq (α := ℂ)
    (((conjugate (extensionEmbedding w)).comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ) x : ℂ)
    ((extensionEmbedding v : (a : v.Completion) → ℂ) x : ℂ)
have a₁ : ∀ (a : WithAbs (↑v : AbsoluteValue K ℝ)),
  Eq (α := ℂ)
    (((conjugate (extensionEmbedding w)).comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ)
        (↑a : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ))) :
      ℂ)
    ((extensionEmbedding v : (a : v.Completion) → ℂ) (↑a : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ))) :
      ℂ)
Tactic: induction x using induction_on
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances (goal)
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 : K
⊢ Eq.{u_2 + 1} (α := w.Completion) ((algebraMap K w.Completion : (a : K) → w.Completion) x : w.Completion)
    ((algebraMap v.Completion w.Completion : (a : v.Completion) → w.Completion)
        ((algebraMap K v.Completion : (a : K) → v.Completion) x) :
      w.Completion)
have simp_rw : Eq.{u_2 + 1} (α := w.Completion)
  ((↑((algebraMap K (WithAbs (↑w : AbsoluteValue L ℝ)) : (a : K) → WithAbs (↑w : AbsoluteValue L ℝ)) x) :
      UniformSpace.Completion (WithAbs (↑w : AbsoluteValue L ℝ))) :
    UniformSpace.Completion (WithAbs (↑w : AbsoluteValue L ℝ)))
  ((↑((algebraMap (WithAbs (↑v : AbsoluteValue K ℝ)) (WithAbs (↑w : AbsoluteValue L ℝ)) :
            (a : WithAbs (↑v : AbsoluteValue K ℝ)) → WithAbs (↑w : AbsoluteValue L ℝ))
          ((algebraMap K (WithAbs (↑v : AbsoluteValue K ℝ)) : (a : K) → WithAbs (↑v : AbsoluteValue K ℝ)) x)) :
      UniformSpace.Completion (WithAbs (↑w : AbsoluteValue L ℝ))) :
    UniformSpace.Completion (WithAbs (↑w : AbsoluteValue L ℝ)))
Tactic: simp_rw [RingHom.algebraMap_toAlgebra, UniformSpace.Completion.algebraMap_def,
      Isometry.mapRingHom_coe]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.Ramification (hypothesis)
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
⊢ Module.finrank.{u_1, u_2} v.Completion w.Completion = 2
have H : w.IsComplex ∧ IsReal (w.comap (algebraMap K L))
Tactic: have H := NumberField.InfinitePlace.isRamified_iff.mp h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.Ramification (hypothesis)
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 ∧ IsReal (w.comap (algebraMap K L))
⊢ Module.finrank.{u_1, u_2} v.Completion w.Completion = 2
have H₁ : w.IsComplex ∧ v.IsReal
Tactic: rw [NumberField.InfinitePlace.LiesOver.comap_eq w v] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.Ramification (hypothesis)
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
⊢ Module.finrank.{u_1, u_2} v.Completion w.Completion = 2
have this : ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)
Tactic: have := LiesOver.extensionEmbedding_liesOver_of_isReal w H.2
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.Ramification (goal)
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)
⊢ RingHom.comp (algebraMap ℝ ℂ) (ringEquivRealOfIsReal ⋯).toRingHom =
    (ringEquivComplexOfIsComplex ⋯).toRingHom.comp (algebraMap v.Completion w.Completion)
have a : ∀ (x : v.Completion),
  Eq (α := ℂ) ((RingHom.comp (algebraMap ℝ ℂ) (ringEquivRealOfIsReal sorry).toRingHom : (a : v.Completion) → ℂ) x : ℂ)
    (((ringEquivComplexOfIsComplex sorry).toRingHom.comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ)
        x :
      ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.Ramification (goal)
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)
⊢ Module.finrank.{u_1, u_2} v.Completion w.Completion = 2
have rw : Module.finrank ℝ ℂ = 2
Tactic: rw [Algebra.finrank_eq_of_equiv_equiv (ringEquivRealOfIsReal H.2)
      (ringEquivComplexOfIsComplex H.1) (by ext; simp),
    Complex.finrank_real_complex]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.Ramification (goal)
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
⊢ Module.finrank.{u_1, u_2} v.Completion w.Completion = 2
have rw₁ : Eq (α := ℕ) 2 2
Tactic: rw [Algebra.finrank_eq_of_equiv_equiv (ringEquivRealOfIsReal H.2)
      (ringEquivComplexOfIsComplex H.1) (by ext; simp),
    Complex.finrank_real_complex]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.Ramification (goal)
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
⊢ Module.finrank.{u_1, u_2} v.Completion w.Completion = 1
have inl : ∀ (hv : v.IsReal), Module.finrank.{u_1, u_2} v.Completion w.Completion = 1
Tactic: rcases v.isReal_or_isComplex with (hv | hv)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.Ramification (goal)
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
⊢ Module.finrank.{u_1, u_2} v.Completion w.Completion = 1
have inr : ∀ (hv : v.IsComplex), Module.finrank.{u_1, u_2} v.Completion w.Completion = 1
Tactic: rcases v.isReal_or_isComplex with (hv | hv)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.Ramification (hypothesis)
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
⊢ Module.finrank.{u_1, u_2} v.Completion w.Completion = 1
have this : ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)
Tactic: have := LiesOver.extensionEmbedding_liesOver_of_isReal w hv
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.Ramification (goal)
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)
⊢ Module.finrank.{u_1, u_2} v.Completion w.Completion = 1
have inl : Module.finrank ℝ ℝ = 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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.Ramification (goal)
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
⊢ Module.finrank.{u_1, u_2} v.Completion w.Completion = 1
have inl₁ : Eq (α := ℕ) 1 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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.Ramification (hypothesis)
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
⊢ Module.finrank.{u_1, u_2} v.Completion w.Completion = 1
have this : ComplexEmbedding.LiesOver w.embedding v.embedding
Tactic: have : ComplexEmbedding.LiesOver w.embedding v.embedding := ⟨hl⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.Ramification (hypothesis)
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
⊢ Module.finrank.{u_1, u_2} v.Completion w.Completion = 1
have this₁ : ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)
Tactic: have := liesOver_extensionEmbedding w v
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.Ramification (goal)
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)
⊢ RingHom.comp (algebraMap ℂ ℂ) (ringEquivComplexOfIsComplex hv).toRingHom =
    (ringEquivComplexOfIsComplex ⋯).toRingHom.comp (algebraMap v.Completion w.Completion)
have a : ∀ (x : v.Completion),
  Eq (α := ℂ)
    ((RingHom.comp (algebraMap ℂ ℂ) (ringEquivComplexOfIsComplex hv).toRingHom : (a : v.Completion) → ℂ) x : ℂ)
    (((ringEquivComplexOfIsComplex sorry).toRingHom.comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ)
        x :
      ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.Ramification (goal)
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)
⊢ Module.finrank.{u_1, u_2} v.Completion w.Completion = 1
have inr : Module.finrank ℂ ℂ = 1
Tactic: rw [Algebra.finrank_eq_of_equiv_equiv (ringEquivComplexOfIsComplex hv)
          (ringEquivComplexOfIsComplex (LiesOver.isComplex_of_isComplex_under _ hv)) (by ext; simp),
        Module.finrank_self]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.Ramification (goal)
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
⊢ Module.finrank.{u_1, u_2} v.Completion w.Completion = 1
have inr₁ : Eq (α := ℕ) 1 1
Tactic: rw [Algebra.finrank_eq_of_equiv_equiv (ringEquivComplexOfIsComplex hv)
          (ringEquivComplexOfIsComplex (LiesOver.isComplex_of_isComplex_under _ hv)) (by ext; simp),
        Module.finrank_self]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.Ramification (hypothesis)
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
⊢ Module.finrank.{u_1, u_2} v.Completion w.Completion = 1
have this : ComplexEmbedding.LiesOver (conjugate w.embedding) v.embedding
Tactic: have : ComplexEmbedding.LiesOver (conjugate w.embedding) v.embedding := ⟨hr⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.Ramification (hypothesis)
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
⊢ Module.finrank.{u_1, u_2} v.Completion w.Completion = 1
have this₁ : ComplexEmbedding.LiesOver (conjugate (extensionEmbedding w)) (extensionEmbedding v)
Tactic: have := liesOver_conjugate_extensionEmbedding w v
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.Ramification (goal)
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)
⊢ RingHom.comp (algebraMap ℂ ℂ) (ringEquivComplexOfIsComplex hv).toRingHom =
    ((ringEquivComplexOfIsComplex ⋯).trans starRingAut).toRingHom.comp (algebraMap v.Completion w.Completion)
have a : ∀ (x : v.Completion),
  Eq (α := ℂ)
    ((RingHom.comp (algebraMap ℂ ℂ) (ringEquivComplexOfIsComplex hv).toRingHom : (a : v.Completion) → ℂ) x : ℂ)
    ((((ringEquivComplexOfIsComplex sorry).trans starRingAut).toRingHom.comp (algebraMap v.Completion w.Completion) :
          (a : v.Completion) → ℂ)
        x :
      ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.Ramification (goal)
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)
⊢ Module.finrank.{u_1, u_2} v.Completion w.Completion = 1
have inr : Module.finrank ℂ ℂ = 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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.Ramification (goal)
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
⊢ Module.finrank.{u_1, u_2} v.Completion w.Completion = 1
have inr₁ : Eq (α := ℕ) 1 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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.Ramification (hypothesis)
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
⊢ Module.finrank.{u_1, u_2} v.Completion w.Completion = 1
have x : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.Ramification (goal)
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 = Module.finrank.{u_1, u_2} v.Completion w.Completion
have 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
Tactic: simp only [inertiaDeg_of_liesOver, Ideal.inertiaDeg, Ideal.comap_bot_of_injective _ <|
    FaithfulSMul.algebraMap_injective v.Completion w.Completion]