awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
inst_3 : Algebra.IsAlgebraic k K
φ : k →+* ℂ
this : Algebra k ℂ := φ.toAlgebra
rw : @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑IsAlgClosed.lift : K →+* ℂ) (algebraMap k K) = φ
⊢ @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (AlgHom.toRingHom.{u_2, u_1, 0} (R := k) IsAlgClosed.lift)
      (algebraMap k K) =
    φ
have rw₁ : algebraMap k ℂ = φ
Tactic: rw [AlgHom.toRingHom_eq_coe, AlgHom.comp_algebraMap_of_tower, RingHom.algebraMap_toAlgebra']
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
inst_3 : Algebra.IsAlgebraic k K
φ : k →+* ℂ
this : Algebra k ℂ := φ.toAlgebra
rw : @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑IsAlgClosed.lift : K →+* ℂ) (algebraMap k K) = φ
rw₁ : algebraMap k ℂ = φ
⊢ @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (AlgHom.toRingHom.{u_2, u_1, 0} (R := k) IsAlgClosed.lift)
      (algebraMap k K) =
    φ
have rw₂ : φ = φ
Tactic: rw [AlgHom.toRingHom_eq_coe, AlgHom.comp_algebraMap_of_tower, RingHom.algebraMap_toAlgebra']
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
⊢ place (conjugate φ) = place φ
have a : ∀ (x : K), Eq (α := ℝ) ((place (conjugate φ) : (a : K) → ℝ) x : ℝ) ((place φ : (a : K) → ℝ) x : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ (↑((hφ.embedding : (a : K) → ℝ) x) : ℂ) = (φ : (a : K) → ℂ) x
have a : (↑((hφ.embedding : (a : K) → ℝ) x) : ℂ).re = re ((φ : (a : K) → ℂ) x)
Tactic: apply Complex.ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
a : (↑((hφ.embedding : (a : K) → ℝ) x) : ℂ).re = re ((φ : (a : K) → ℂ) x)
⊢ (↑((hφ.embedding : (a : K) → ℝ) x) : ℂ) = (φ : (a : K) → ℂ) x
have a₁ : (↑((hφ.embedding : (a : K) → ℝ) x) : ℂ).im = im ((φ : (a : K) → ℂ) x)
Tactic: apply Complex.ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ (↑((hφ.embedding : (a : K) → ℝ) x) : ℂ).im = im ((φ : (a : K) → ℂ) x)
have a : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : K) → ℂ) x : ℂ) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)
Tactic: rw [ofReal_im, eq_comm, ← Complex.conj_eq_iff_im]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
f : k →+* K
φ : K →+* ℂ
hφ : IsReal φ
⊢ IsReal (φ.comp f)
have a : ∀ (x : k), Eq (α := ℂ) ((star (φ.comp f) : (a : k) → ℂ) x : ℂ) ((φ.comp f : (a : k) → ℂ) x : ℂ)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
f : k ≃+* K
φ : K →+* ℂ
H : IsReal (φ.comp (↑f : k →+* K))
⊢ IsReal φ
have h : φ = RingHom.comp (φ.comp (↑f : k →+* K)) f.symm.toRingHom
Tactic: convert! H.comp f.symm.toRingHom
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
f : k ≃+* K
φ : K →+* ℂ
H : IsReal (φ.comp (↑f : k →+* K))
⊢ φ = RingHom.comp (φ.comp (↑f : k →+* K)) f.symm.toRingHom
have h : ∀ (x : K),
  Eq (α := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ((RingHom.comp (φ.comp (↑f : k →+* K)) f.symm.toRingHom : (a : K) → ℂ) x : ℂ)
Tactic: ext1
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (hypothesis)
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))
this_1 : Algebra k ℂ := RingHom.toAlgebra (φ.comp (algebraMap k K))
this : Algebra K ℂ := φ.toAlgebra
⊢ ∃ (σ : Gal(K/k)), φ.comp (↑σ.symm : K →+* K) = ψ
have this₁ : IsScalarTower k K ℂ
Tactic: have : IsScalarTower k K ℂ := IsScalarTower.of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
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))
this_1 : Algebra k ℂ := RingHom.toAlgebra (φ.comp (algebraMap k K))
this_2 : Algebra K ℂ := φ.toAlgebra
this : IsScalarTower k K ℂ
ψ' : K →ₐ[k] ℂ := { toRingHom := ψ, commutes' := ⋯ }
⊢ ∃ (σ : Gal(K/k)), φ.comp (↑σ.symm : K →+* K) = ψ
have h₁ : φ.comp (↑(AlgEquiv.symm (AlgEquiv.symm (ψ'.restrictNormal' K))) : K →+* K) = ψ
Tactic: use (AlgHom.restrictNormal' ψ' K).symm
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
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))
this_1 : Algebra k ℂ := RingHom.toAlgebra (φ.comp (algebraMap k K))
this_2 : Algebra K ℂ := φ.toAlgebra
this : IsScalarTower k K ℂ
ψ' : K →ₐ[k] ℂ := { toRingHom := ψ, commutes' := ⋯ }
⊢ φ.comp (↑(AlgEquiv.symm (AlgEquiv.symm (ψ'.restrictNormal' K))) : K →+* K) = ψ
have h₁ : ∀ (x : K),
  Eq (α := ℂ) ((φ.comp (↑(AlgEquiv.symm (AlgEquiv.symm (ψ'.restrictNormal' K))) : K →+* K) : (a : K) → ℂ) x : ℂ)
    ((ψ : (a : K) → ℂ) x : ℂ)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
h : IsConj φ σ
⊢ IsReal (φ.comp (algebraMap k K))
have a : ∀ (x : k),
  Eq (α := ℂ) ((star (φ.comp (algebraMap k K)) : (a : k) → ℂ) x : ℂ) ((φ.comp (algebraMap k K) : (a : k) → ℂ) x : ℂ)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
hσ : IsConj φ σ
ν : Gal(K/k)
⊢ IsConj (φ.comp (↑ν : K →+* K)) (ν⁻¹ * σ * ν)
have a : ∀ (x : K),
  Eq (α := ℂ) ((conjugate (φ.comp (↑ν : K →+* K)) : (a : K) → ℂ) x : ℂ)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (φ.comp (↑ν : K →+* K)) (↑(ν⁻¹ * σ * ν) : K →+* K) :
          (a : K) → ℂ)
        x :
      ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
hσ : IsConj φ σ
hσ' : σ ≠ 1
⊢ HPow.hPow (β := ℕ) σ 2 = 1
have h : ∀ (a : K), Eq (α := K) ((HPow.hPow (β := ℕ) σ 2 : (a : K) → K) a : K) ((1 : (a : K) → K) a : K)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
F : Type u_3
inst_2 : Field F
w : InfinitePlace K
f : k →+* K
⊢ place (w.embedding.comp f) = (↑w : AbsoluteValue K ℝ).comp (f := f) ⋯
have a : ∀ (x : k),
  Eq (α := ℝ) ((place (w.embedding.comp f) : (a : k) → ℝ) x : ℝ)
    (((↑w : AbsoluteValue K ℝ).comp (f := f) sorry : (a : k) → ℝ) x : ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
F : Type u_3
inst_2 : Field F
w : InfinitePlace K
f : k →+* K
x : k
⊢ Eq (α := ℝ) ((place (w.embedding.comp f) : (a : k) → ℝ) x : ℝ)
    (((↑w : AbsoluteValue K ℝ).comp (f := f) ⋯ : (a : k) → ℝ) x : ℝ)
have a : Eq (α := ℝ) ((place (w.embedding.comp f) : (a : k) → ℝ) x : ℝ)
  (((↑w : AbsoluteValue K ℝ) : (a : K) → ℝ) ((f : (a : k) → K) x : K) : ℝ)
Tactic: change _ = w.1 (f x)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
F : Type u_3
inst_2 : Field F
w : InfinitePlace K
f : k →+* K
x : k
⊢ Eq (α := ℝ) ((place (w.embedding.comp f) : (a : k) → ℝ) x : ℝ)
    (((↑w : AbsoluteValue K ℝ) : (a : K) → ℝ) ((f : (a : k) → K) x : K) : ℝ)
have a : Eq (α := ℝ) ((place (w.embedding.comp f) : (a : k) → ℝ) x : ℝ)
  ((place (sorry.choose (p := fun (φ : K →+* ℂ) ↦ place φ = (↑w : AbsoluteValue K ℝ))) : (a : K) → ℝ)
      ((f : (a : k) → K) x : K) :
    ℝ)
Tactic: rw [← w.2.choose_spec]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
F : Type u_3
inst_2 : Field F
w : InfinitePlace K
f : k →+* K
⊢ place (w.embedding.comp f) = (↑w : AbsoluteValue K ℝ).comp (f := f) ⋯
have a : ∀ (x : k),
  Eq (α := ℝ) ((place (w.embedding.comp f) : (a : k) → ℝ) x : ℝ)
    (((↑w : AbsoluteValue K ℝ).comp (f := f) sorry : (a : k) → ℝ) x : ℝ)
Tactic: { ext x; change _ = w.1 (f x); rw [← w.2.choose_spec]; rfl }
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
F : Type u_3
inst_2 : Field F
w : InfinitePlace K
f : k →+* K
a a₁ :
  ∀ (x : k),
    Eq (α := ℝ) ((place (w.embedding.comp f) : (a : k) → ℝ) x : ℝ)
      (((↑w : AbsoluteValue K ℝ).comp (f := f) ⋯ : (a : k) → ℝ) x : ℝ)
⊢ place (w.embedding.comp f) = (↑w : AbsoluteValue K ℝ).comp (f := f) ⋯
have a₂ : ∀ (x : k),
  Eq (α := ℝ) ((place (w.embedding.comp f) : (a : k) → ℝ) x : ℝ)
    (((↑w : AbsoluteValue K ℝ) : (a : K) → ℝ) ((f : (a : k) → K) x : K) : ℝ)
Tactic: { ext x; change _ = w.1 (f x); rw [← w.2.choose_spec]; rfl }
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
F : Type u_3
inst_2 : Field F
w : InfinitePlace K
f : k →+* K
a a₁ :
  ∀ (x : k),
    Eq (α := ℝ) ((place (w.embedding.comp f) : (a : k) → ℝ) x : ℝ)
      (((↑w : AbsoluteValue K ℝ).comp (f := f) ⋯ : (a : k) → ℝ) x : ℝ)
a₂ a₃ :
  ∀ (x : k),
    Eq (α := ℝ) ((place (w.embedding.comp f) : (a : k) → ℝ) x : ℝ)
      (((↑w : AbsoluteValue K ℝ) : (a : K) → ℝ) ((f : (a : k) → K) x : K) : ℝ)
⊢ place (w.embedding.comp f) = (↑w : AbsoluteValue K ℝ).comp (f := f) ⋯
have a₄ : ∀ (x : k),
  Eq (α := ℝ) ((place (w.embedding.comp f) : (a : k) → ℝ) x : ℝ)
    ((place (sorry.choose (p := fun (φ : K →+* ℂ) ↦ place φ = (↑w : AbsoluteValue K ℝ))) : (a : K) → ℝ)
        ((f : (a : k) → K) x : K) :
      ℝ)
Tactic: { ext x; change _ = w.1 (f x); rw [← w.2.choose_spec]; rfl }
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
hφ : w.IsReal
⊢ (w.comap f).IsReal
have rw : ComplexEmbedding.IsReal (w.embedding.comp f)
Tactic: rw [← mk_embedding w, comap_mk, isReal_mk_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (hypothesis)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
hφ : w.IsReal
⊢ ComplexEmbedding.IsReal (w.embedding.comp f)
have hφ₁ : ComplexEmbedding.IsReal w.embedding
Tactic: rw [← mk_embedding w, isReal_mk_iff] at hφ
Cleared hypotheses: hφ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
hf : (w.comap f).IsComplex
⊢ w.IsComplex
have rw : ∀ (hf : ¬(w.comap f).IsReal), ¬w.IsReal
Tactic: rw [← not_isReal_iff_isComplex] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k ≃+* K
w : InfinitePlace K
⊢ IsReal (w.comap (↑f : k →+* K)) ↔ w.IsReal
have rw : IsReal ((mk w.embedding).comap (↑f : k →+* K)) ↔ (mk w.embedding).IsReal
Tactic: rw [← mk_embedding w, comap_mk, isReal_mk_iff, isReal_mk_iff, ComplexEmbedding.isReal_comp_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k ≃+* K
w : InfinitePlace K
rw : IsReal ((mk w.embedding).comap (↑f : k →+* K)) ↔ (mk w.embedding).IsReal
⊢ IsReal (w.comap (↑f : k →+* K)) ↔ w.IsReal
have rw₁ : IsReal (mk (w.embedding.comp (↑f : k →+* K))) ↔ (mk w.embedding).IsReal
Tactic: rw [← mk_embedding w, comap_mk, isReal_mk_iff, isReal_mk_iff, ComplexEmbedding.isReal_comp_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k ≃+* K
w : InfinitePlace K
rw : IsReal ((mk w.embedding).comap (↑f : k →+* K)) ↔ (mk w.embedding).IsReal
rw₁ : IsReal (mk (w.embedding.comp (↑f : k →+* K))) ↔ (mk w.embedding).IsReal
⊢ IsReal (w.comap (↑f : k →+* K)) ↔ w.IsReal
have rw₂ : ComplexEmbedding.IsReal (w.embedding.comp (↑f : k →+* K)) ↔ (mk w.embedding).IsReal
Tactic: rw [← mk_embedding w, comap_mk, isReal_mk_iff, isReal_mk_iff, ComplexEmbedding.isReal_comp_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k ≃+* K
w : InfinitePlace K
rw : IsReal ((mk w.embedding).comap (↑f : k →+* K)) ↔ (mk w.embedding).IsReal
rw₁ : IsReal (mk (w.embedding.comp (↑f : k →+* K))) ↔ (mk w.embedding).IsReal
rw₂ : ComplexEmbedding.IsReal (w.embedding.comp (↑f : k →+* K)) ↔ (mk w.embedding).IsReal
⊢ IsReal (w.comap (↑f : k →+* K)) ↔ w.IsReal
have rw₃ : ComplexEmbedding.IsReal (w.embedding.comp (↑f : k →+* K)) ↔ ComplexEmbedding.IsReal w.embedding
Tactic: rw [← mk_embedding w, comap_mk, isReal_mk_iff, isReal_mk_iff, ComplexEmbedding.isReal_comp_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k ≃+* K
w : InfinitePlace K
rw : IsReal ((mk w.embedding).comap (↑f : k →+* K)) ↔ (mk w.embedding).IsReal
rw₁ : IsReal (mk (w.embedding.comp (↑f : k →+* K))) ↔ (mk w.embedding).IsReal
rw₂ : ComplexEmbedding.IsReal (w.embedding.comp (↑f : k →+* K)) ↔ (mk w.embedding).IsReal
rw₃ : ComplexEmbedding.IsReal (w.embedding.comp (↑f : k →+* K)) ↔ ComplexEmbedding.IsReal w.embedding
⊢ IsReal (w.comap (↑f : k →+* K)) ↔ w.IsReal
have rw₄ : ComplexEmbedding.IsReal w.embedding ↔ ComplexEmbedding.IsReal w.embedding
Tactic: rw [← mk_embedding w, comap_mk, isReal_mk_iff, isReal_mk_iff, ComplexEmbedding.isReal_comp_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
h : (w.comap f).IsReal
⊢ ComplexEmbedding.IsReal (w.embedding.comp f)
have rwa : (mk (w.embedding.comp f)).IsReal
Tactic: rwa [← isReal_mk_iff, ← comap_mk, mk_embedding]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
h : (w.comap f).IsReal
rwa : (mk (w.embedding.comp f)).IsReal
⊢ ComplexEmbedding.IsReal (w.embedding.comp f)
have rwa₁ : ((mk w.embedding).comap f).IsReal
Tactic: rwa [← isReal_mk_iff, ← comap_mk, mk_embedding]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
h : (w.comap f).IsReal
⊢ (w.comap f).embedding = w.embedding.comp f
have rw : ((mk w.embedding).comap f).embedding = (mk w.embedding).embedding.comp f
Tactic: rw [← mk_embedding w, comap_mk, mk_embedding, embedding_mk_eq_of_isReal
    (by rwa [← isReal_mk_iff, ← comap_mk, mk_embedding])]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
h : (w.comap f).IsReal
rw : ((mk w.embedding).comap f).embedding = (mk w.embedding).embedding.comp f
⊢ (w.comap f).embedding = w.embedding.comp f
have rw₁ : (mk (w.embedding.comp f)).embedding = (mk w.embedding).embedding.comp f
Tactic: rw [← mk_embedding w, comap_mk, mk_embedding, embedding_mk_eq_of_isReal
    (by rwa [← isReal_mk_iff, ← comap_mk, mk_embedding])]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
h : (w.comap f).IsReal
rw : ((mk w.embedding).comap f).embedding = (mk w.embedding).embedding.comp f
rw₁ : (mk (w.embedding.comp f)).embedding = (mk w.embedding).embedding.comp f
⊢ (w.comap f).embedding = w.embedding.comp f
have rw₂ : (mk (w.embedding.comp f)).embedding = w.embedding.comp f
Tactic: rw [← mk_embedding w, comap_mk, mk_embedding, embedding_mk_eq_of_isReal
    (by rwa [← isReal_mk_iff, ← comap_mk, mk_embedding])]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
h : (w.comap f).IsReal
rw : ((mk w.embedding).comap f).embedding = (mk w.embedding).embedding.comp f
rw₁ : (mk (w.embedding.comp f)).embedding = (mk w.embedding).embedding.comp f
rw₂ : (mk (w.embedding.comp f)).embedding = w.embedding.comp f
⊢ (w.comap f).embedding = w.embedding.comp f
have rw₃ : w.embedding.comp f = w.embedding.comp f
Tactic: rw [← mk_embedding w, comap_mk, mk_embedding, embedding_mk_eq_of_isReal
    (by rwa [← isReal_mk_iff, ← comap_mk, mk_embedding])]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
⊢ LE.le (α := ℕ) (if (w.comap f).IsReal then 1 else 2) (if w.IsReal then 1 else 2)
have pos : ∀ (h₁ : (w.comap f).IsReal) (h₂ : w.IsReal), LE.le (α := ℕ) 1 1
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
pos : ∀ (h₁ : (w.comap f).IsReal) (h₂ : w.IsReal), LE.le (α := ℕ) 1 1
⊢ LE.le (α := ℕ) (if (w.comap f).IsReal then 1 else 2) (if w.IsReal then 1 else 2)
have neg : ∀ (h₁ : (w.comap f).IsReal) (h₂ : ¬w.IsReal), LE.le (α := ℕ) 1 2
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
pos : ∀ (h₁ : (w.comap f).IsReal) (h₂ : w.IsReal), LE.le (α := ℕ) 1 1
neg : ∀ (h₁ : (w.comap f).IsReal) (h₂ : ¬w.IsReal), LE.le (α := ℕ) 1 2
⊢ LE.le (α := ℕ) (if (w.comap f).IsReal then 1 else 2) (if w.IsReal then 1 else 2)
have pos₁ : ∀ (h₁ : ¬(w.comap f).IsReal) (h₂ : w.IsReal), LE.le (α := ℕ) 2 1
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
f : k →+* K
w : InfinitePlace K
pos : ∀ (h₁ : (w.comap f).IsReal) (h₂ : w.IsReal), LE.le (α := ℕ) 1 1
neg : ∀ (h₁ : (w.comap f).IsReal) (h₂ : ¬w.IsReal), LE.le (α := ℕ) 1 2
pos₁ : ∀ (h₁ : ¬(w.comap f).IsReal) (h₂ : w.IsReal), LE.le (α := ℕ) 2 1
⊢ LE.le (α := ℕ) (if (w.comap f).IsReal then 1 else 2) (if w.IsReal then 1 else 2)
have neg₁ : ∀ (h₁ : ¬(w.comap f).IsReal) (h₂ : ¬w.IsReal), LE.le (α := ℕ) 2 2
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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).IsComplex ↔ w.IsComplex
have rw : ¬(σ • w).IsReal ↔ w.IsComplex
Tactic: rw [← not_isReal_iff_isComplex, ← not_isReal_iff_isComplex, isReal_smul_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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
⊢ (σ • w).IsComplex ↔ w.IsComplex
have rw₁ : ¬(σ • w).IsReal ↔ ¬w.IsReal
Tactic: rw [← not_isReal_iff_isComplex, ← not_isReal_iff_isComplex, isReal_smul_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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
⊢ (σ • w).IsComplex ↔ w.IsComplex
have rw₂ : ¬w.IsReal ↔ ¬w.IsReal
Tactic: rw [← not_isReal_iff_isComplex, ← not_isReal_iff_isComplex, isReal_smul_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (hypothesis)
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))
⊢ ∃ (σ : Gal(K/k)), σ • w = w'
have 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))
Tactic: rw [← mk_embedding w, ← mk_embedding w', comap_mk, comap_mk, mk_eq_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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)), σ • w = w'
have inl : ∀ (σ : Gal(K/k)) (hσ : w.embedding.comp (↑σ.symm : K →+* K) = w'.embedding), ∃ (σ : Gal(K/k)), σ • w = w'
Tactic: obtain ⟨σ, hσ⟩ := ComplexEmbedding.exists_comp_symm_eq_of_comp_eq w.embedding w'.embedding h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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
⊢ ∃ (σ : Gal(K/k)), σ • w = w'
have h₁ : σ • w = w'
Tactic: use σ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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
⊢ σ • w = w'
have h₁ : σ • mk w.embedding = w'
Tactic: rw [← mk_embedding w, ← mk_embedding w', smul_mk, hσ]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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'
⊢ σ • w = w'
have h₂ : σ • mk w.embedding = mk w'.embedding
Tactic: rw [← mk_embedding w, ← mk_embedding w', smul_mk, hσ]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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
⊢ σ • w = w'
have h₃ : mk (w.embedding.comp (↑σ.symm : K →+* K)) = mk w'.embedding
Tactic: rw [← mk_embedding w, ← mk_embedding w', smul_mk, hσ]