-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma exists_smul_eq_of_comap_eq [IsGalois k K] {w w' : InfinitePlace K}
    (h : w.comap (algebraMap k K) = w'.comap (algebraMap k K)) : ∃ σ : K ≃ₐ[k] K, σ • w = w'

Proof state:
case h
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w w' : InfinitePlace K
h : ComplexEmbedding.conjugate (w.embedding.comp (algebraMap k K)) = w'.embedding.comp (algebraMap k K)
σ : K ≃ₐ[k] K
hσ : ((starRingEnd ℂ).comp w.embedding).comp ↑σ.symm = w'.embedding
⊢ w.embedding.comp ↑σ.symm = w'.embedding ∨ ComplexEmbedding.conjugate (w.embedding.comp ↑σ.symm) = w'.embedding

Tactic:
exact Or.inr hσ

Result:
no goals

Proof state:
case h
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w w' : InfinitePlace K
h : ComplexEmbedding.conjugate (w.embedding.comp (algebraMap k K)) = w'.embedding.comp (algebraMap k K)
σ : K ≃ₐ[k] K
hσ : ((starRingEnd ℂ).comp w.embedding).comp ↑σ.symm = w'.embedding
⊢ σ • w = w'

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

Result:
case h
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w w' : InfinitePlace K
h : ComplexEmbedding.conjugate (w.embedding.comp (algebraMap k K)) = w'.embedding.comp (algebraMap k K)
σ : K ≃ₐ[k] K
hσ : ((starRingEnd ℂ).comp w.embedding).comp ↑σ.symm = w'.embedding
⊢ w.embedding.comp ↑σ.symm = w'.embedding ∨ ComplexEmbedding.conjugate (w.embedding.comp ↑σ.symm) = w'.embedding

Proof state:
case inr
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w w' : InfinitePlace K
h : ComplexEmbedding.conjugate (w.embedding.comp (algebraMap k K)) = w'.embedding.comp (algebraMap k K)
⊢ ∃ σ, σ • w = w'

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

Result:
case inr.intro
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w w' : InfinitePlace K
h : ComplexEmbedding.conjugate (w.embedding.comp (algebraMap k K)) = w'.embedding.comp (algebraMap k K)
σ : K ≃ₐ[k] K
hσ : ((starRingEnd ℂ).comp w.embedding).comp ↑σ.symm = w'.embedding
⊢ ∃ σ, σ • w = w'

Proof state:
case inr.intro
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w w' : InfinitePlace K
h : ComplexEmbedding.conjugate (w.embedding.comp (algebraMap k K)) = w'.embedding.comp (algebraMap k K)
σ : K ≃ₐ[k] K
hσ : ((starRingEnd ℂ).comp w.embedding).comp ↑σ.symm = w'.embedding
⊢ ∃ σ, σ • w = w'

Tactic:
use σ

Result:
case h
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w w' : InfinitePlace K
h : ComplexEmbedding.conjugate (w.embedding.comp (algebraMap k K)) = w'.embedding.comp (algebraMap k K)
σ : K ≃ₐ[k] K
hσ : ((starRingEnd ℂ).comp w.embedding).comp ↑σ.symm = w'.embedding
⊢ σ • w = w'

Proof state:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w w' : InfinitePlace K
h :
  w.embedding.comp (algebraMap k K) = w'.embedding.comp (algebraMap k K) ∨
    ComplexEmbedding.conjugate (w.embedding.comp (algebraMap k K)) = w'.embedding.comp (algebraMap 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σ

Result:
no goals

Proof state:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w w' : InfinitePlace K
h : w.comap (algebraMap k K) = w'.comap (algebraMap k K)
⊢ ∃ σ, σ • w = w'

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

Result:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w w' : InfinitePlace K
h :
  w.embedding.comp (algebraMap k K) = w'.embedding.comp (algebraMap k K) ∨
    ComplexEmbedding.conjugate (w.embedding.comp (algebraMap k K)) = w'.embedding.comp (algebraMap k K)
⊢ ∃ σ, σ • w = w'

Proof state:
case inl.intro
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w w' : InfinitePlace K
h : w.embedding.comp (algebraMap k K) = w'.embedding.comp (algebraMap k K)
σ : K ≃ₐ[k] K
hσ : w.embedding.comp ↑σ.symm = w'.embedding
⊢ ∃ σ, σ • w = w'

Tactic:
use σ

Result:
case h
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w w' : InfinitePlace K
h : w.embedding.comp (algebraMap k K) = w'.embedding.comp (algebraMap k K)
σ : K ≃ₐ[k] K
hσ : w.embedding.comp ↑σ.symm = w'.embedding
⊢ σ • w = w'

Proof state:
case inl
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w w' : InfinitePlace K
h : w.embedding.comp (algebraMap k K) = w'.embedding.comp (algebraMap k K)
⊢ ∃ σ, σ • w = w'

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

Result:
case inl.intro
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w w' : InfinitePlace K
h : w.embedding.comp (algebraMap k K) = w'.embedding.comp (algebraMap k K)
σ : K ≃ₐ[k] K
hσ : w.embedding.comp ↑σ.symm = w'.embedding
⊢ ∃ σ, σ • w = w'

Proof state:
case h
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w w' : InfinitePlace K
h : w.embedding.comp (algebraMap k K) = w'.embedding.comp (algebraMap k K)
σ : K ≃ₐ[k] K
hσ : w.embedding.comp ↑σ.symm = w'.embedding
⊢ σ • w = w'

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

Result:
no goals