awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h₃ : mk (w.embedding.comp (↑σ.symm : K →+* K)) = mk w'.embedding
⊢ σ • 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 →+* ℂ) (conjugate (w.embedding.comp (algebraMap k K))) (w'.embedding.comp (algebraMap k K))
⊢ ∃ (σ : Gal(K/k)), σ • w = w'
have inr : ∀ (σ : Gal(K/k)) (hσ : (RingHom.comp (starRingEnd ℂ) w.embedding).comp (↑σ.symm : K →+* K) = w'.embedding),
  ∃ (σ : Gal(K/k)), σ • w = w'
Tactic: obtain ⟨σ, hσ⟩ := ComplexEmbedding.exists_comp_symm_eq_of_comp_eq
      ((starRingEnd ℂ).comp (embedding w)) 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 →+* ℂ) (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
⊢ ∃ (σ : 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 →+* ℂ) (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 = w'
have h₁ : w.embedding.comp (↑σ.symm : K →+* K) = w'.embedding ∨ conjugate (w.embedding.comp (↑σ.symm : K →+* K)) = w'.embedding
Tactic: rw [← mk_embedding w, ← mk_embedding w', smul_mk, mk_eq_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
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))
⊢ ∃ (σ : Gal(K/k)), σ • w = w'
have inl : ∀ (h : Eq (α := k →+* ℂ) (w.embedding.comp (algebraMap k K)) (w'.embedding.comp (algebraMap k K))),
  ∃ (σ : 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σ
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)) ∨
    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'
⊢ ∃ (σ : Gal(K/k)), σ • w = w'
have inr : ∀ (h : Eq (α := k →+* ℂ) (conjugate (w.embedding.comp (algebraMap k K))) (w'.embedding.comp (algebraMap k K))),
  ∃ (σ : 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σ
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
⊢ w' ∈ MulAction.orbit Gal(K/k) w ↔ Eq (α := InfinitePlace k) (w.comap (algebraMap k K)) (w'.comap (algebraMap k K))
have refine : 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⟩
-- 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 : InfinitePlace K
σ : Gal(K/k)
⊢ Eq (α := InfinitePlace k) (w.comap (algebraMap k K)) ((σ • w).comap (algebraMap k K))
have 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)))
Tactic: rw [← mk_embedding w, comap_mk, smul_mk, comap_mk]
-- 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 : InfinitePlace K
σ : Gal(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)))
have e_φ : Eq (α := k →+* ℂ) (w.embedding.comp (algebraMap k K))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (w.embedding.comp (↑σ.symm : K →+* K)) (algebraMap k K))
Tactic: congr 1
-- 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 : InfinitePlace K
σ : Gal(K/k)
⊢ Eq (α := k →+* ℂ) (w.embedding.comp (algebraMap k K))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (w.embedding.comp (↑σ.symm : K →+* K)) (algebraMap k K))
have 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 :
      ℂ)
Tactic: ext1
-- 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
inst_3 : Algebra k K
σ : Gal(K/k)
w : InfinitePlace K
inst_4 : IsGalois k K
⊢ Equiv.{u_2 + 1, u_1 + 1} (Quotient (α := InfinitePlace K) (MulAction.orbitRel Gal(K/k) (InfinitePlace K)))
    (InfinitePlace k)
have 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)) sorry)
Tactic: refine Equiv.ofBijective (Quotient.lift (comap · (algebraMap k K))
    fun _ _ e ↦ (mem_orbit_iff.mp e).symm) ⟨?_, ?_⟩
-- 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
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)) ⋯)
⊢ Equiv.{u_2 + 1, u_1 + 1} (Quotient (α := InfinitePlace K) (MulAction.orbitRel Gal(K/k) (InfinitePlace K)))
    (InfinitePlace k)
have 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)) sorry)
Tactic: refine Equiv.ofBijective (Quotient.lift (comap · (algebraMap k K))
    fun _ _ e ↦ (mem_orbit_iff.mp e).symm) ⟨?_, ?_⟩
-- 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
inst_3 : Algebra k K
σ : Gal(K/k)
w_1 : InfinitePlace K
inst_4 : IsGalois k K
w : InfinitePlace k
⊢ ∃ (a : Quotient (α := InfinitePlace K) (MulAction.orbitRel Gal(K/k) (InfinitePlace K))),
    Quotient.lift (fun (x : InfinitePlace K) ↦ x.comap (algebraMap k K)) ⋯ a = w
have 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)) sorry a = w
Tactic: obtain ⟨w', hw⟩ := comap_surjective (K := K) w
-- 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
w : InfinitePlace K
⊢ IsUnramified k w ↔ w.mult ≤ mult (w.comap (algebraMap k K))
have rw : mult (w.comap (algebraMap k K)) ≤ w.mult
Tactic: rw [IsUnramified, le_antisymm_iff, and_iff_right]
-- 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
inst_3 : Algebra k K
inst_4 : Algebra k F
w : InfinitePlace F
h : IsUnramified k w
f : K →ₐ[k] F
⊢ IsUnramified k (w.comap (↑f : K →+* F))
have rw : mult (w.comap (↑f : K →+* F)) ≤ w.mult
Tactic: rw [InfinitePlace.isUnramified_iff_mult_le, ← InfinitePlace.comap_comp, f.comp_algebraMap, h.eq]
-- 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
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
⊢ IsUnramified K w
have rw : mult (comap (w.comap (algebraMap K F)) (algebraMap k K)) ≤ mult (w.comap (algebraMap K F))
Tactic: rw [InfinitePlace.isUnramified_iff_mult_le, ← h.eq, IsScalarTower.algebraMap_eq k K F,
    InfinitePlace.comap_comp]
-- 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
w : InfinitePlace K
⊢ ¬IsUnramified k w ↔ w.IsComplex ∧ IsReal (w.comap (algebraMap k K))
have rw : ¬Eq (α := ℕ) (if IsReal (w.comap (algebraMap k K)) then 1 else 2) (if w.IsReal then 1 else 2) ↔
  ¬w.IsReal ∧ IsReal (w.comap (algebraMap k K))
Tactic: rw [IsUnramified, mult, mult, ← not_isReal_iff_isComplex]
-- 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
w : InfinitePlace K
⊢ ¬Eq (α := ℕ) (if IsReal (w.comap (algebraMap k K)) then 1 else 2) (if w.IsReal then 1 else 2) ↔
    ¬w.IsReal ∧ IsReal (w.comap (algebraMap k K))
have pos : ∀ (h₁ : IsReal (w.comap (algebraMap k K))) (h₂ : w.IsReal),
  ¬Eq (α := ℕ) 1 1 ↔ ¬w.IsReal ∧ IsReal (w.comap (algebraMap k K))
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
w : InfinitePlace K
pos :
  ∀ (h₁ : IsReal (w.comap (algebraMap k K))) (h₂ : w.IsReal),
    ¬Eq (α := ℕ) 1 1 ↔ ¬w.IsReal ∧ IsReal (w.comap (algebraMap k K))
⊢ ¬Eq (α := ℕ) (if IsReal (w.comap (algebraMap k K)) then 1 else 2) (if w.IsReal then 1 else 2) ↔
    ¬w.IsReal ∧ IsReal (w.comap (algebraMap k K))
have neg : ∀ (h₁ : IsReal (w.comap (algebraMap k K))) (h₂ : ¬w.IsReal),
  ¬Eq (α := ℕ) 1 2 ↔ ¬w.IsReal ∧ IsReal (w.comap (algebraMap k K))
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
w : InfinitePlace K
pos :
  ∀ (h₁ : IsReal (w.comap (algebraMap k K))) (h₂ : w.IsReal),
    ¬Eq (α := ℕ) 1 1 ↔ ¬w.IsReal ∧ IsReal (w.comap (algebraMap k K))
neg :
  ∀ (h₁ : IsReal (w.comap (algebraMap k K))) (h₂ : ¬w.IsReal),
    ¬Eq (α := ℕ) 1 2 ↔ ¬w.IsReal ∧ IsReal (w.comap (algebraMap k K))
⊢ ¬Eq (α := ℕ) (if IsReal (w.comap (algebraMap k K)) then 1 else 2) (if w.IsReal then 1 else 2) ↔
    ¬w.IsReal ∧ IsReal (w.comap (algebraMap k K))
have pos₁ : ∀ (h₁ : ¬IsReal (w.comap (algebraMap k K))) (h₂ : w.IsReal),
  ¬Eq (α := ℕ) 2 1 ↔ ¬w.IsReal ∧ IsReal (w.comap (algebraMap k K))
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
w : InfinitePlace K
pos :
  ∀ (h₁ : IsReal (w.comap (algebraMap k K))) (h₂ : w.IsReal),
    ¬Eq (α := ℕ) 1 1 ↔ ¬w.IsReal ∧ IsReal (w.comap (algebraMap k K))
neg :
  ∀ (h₁ : IsReal (w.comap (algebraMap k K))) (h₂ : ¬w.IsReal),
    ¬Eq (α := ℕ) 1 2 ↔ ¬w.IsReal ∧ IsReal (w.comap (algebraMap k K))
pos₁ :
  ∀ (h₁ : ¬IsReal (w.comap (algebraMap k K))) (h₂ : w.IsReal),
    ¬Eq (α := ℕ) 2 1 ↔ ¬w.IsReal ∧ IsReal (w.comap (algebraMap k K))
⊢ ¬Eq (α := ℕ) (if IsReal (w.comap (algebraMap k K)) then 1 else 2) (if w.IsReal then 1 else 2) ↔
    ¬w.IsReal ∧ IsReal (w.comap (algebraMap k K))
have neg₁ : ∀ (h₁ : ¬IsReal (w.comap (algebraMap k K))) (h₂ : ¬w.IsReal),
  ¬Eq (α := ℕ) 2 2 ↔ ¬w.IsReal ∧ IsReal (w.comap (algebraMap k K))
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
w : InfinitePlace K
h₁ : ¬IsReal (w.comap (algebraMap k K))
h₂ : w.IsReal
⊢ ¬Eq (α := ℕ) 2 1 ↔ ¬w.IsReal ∧ IsReal (w.comap (algebraMap k K))
have pos : False
Tactic: simp only [not_true_eq_false, false_iff, and_self, forall_true_left, IsEmpty.forall_iff,
      not_and, OfNat.one_ne_ofNat, not_false_eq_true, true_iff, OfNat.ofNat_ne_one, 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
w : InfinitePlace K
⊢ IsUnramified k w ↔ w.IsReal ∨ IsComplex (w.comap (algebraMap k K))
have rw : ¬IsUnramified k w ↔ ¬(w.IsReal ∨ IsComplex (w.comap (algebraMap k K)))
Tactic: rw [← not_iff_not, not_isUnramified_iff, not_or,
    not_isReal_iff_isComplex, not_isComplex_iff_isReal]
-- 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
w : InfinitePlace K
rw : ¬IsUnramified k w ↔ ¬(w.IsReal ∨ IsComplex (w.comap (algebraMap k K)))
⊢ IsUnramified k w ↔ w.IsReal ∨ IsComplex (w.comap (algebraMap k K))
have rw₁ : w.IsComplex ∧ IsReal (w.comap (algebraMap k K)) ↔ ¬(w.IsReal ∨ IsComplex (w.comap (algebraMap k K)))
Tactic: rw [← not_iff_not, not_isUnramified_iff, not_or,
    not_isReal_iff_isComplex, not_isComplex_iff_isReal]
-- 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
w : InfinitePlace K
rw : ¬IsUnramified k w ↔ ¬(w.IsReal ∨ IsComplex (w.comap (algebraMap k K)))
rw₁ : w.IsComplex ∧ IsReal (w.comap (algebraMap k K)) ↔ ¬(w.IsReal ∨ IsComplex (w.comap (algebraMap k K)))
⊢ IsUnramified k w ↔ w.IsReal ∨ IsComplex (w.comap (algebraMap k K))
have rw₂ : w.IsComplex ∧ IsReal (w.comap (algebraMap k K)) ↔ ¬w.IsReal ∧ ¬IsComplex (w.comap (algebraMap k K))
Tactic: rw [← not_iff_not, not_isUnramified_iff, not_or,
    not_isReal_iff_isComplex, not_isComplex_iff_isReal]
-- 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
w : InfinitePlace K
rw : ¬IsUnramified k w ↔ ¬(w.IsReal ∨ IsComplex (w.comap (algebraMap k K)))
rw₁ : w.IsComplex ∧ IsReal (w.comap (algebraMap k K)) ↔ ¬(w.IsReal ∨ IsComplex (w.comap (algebraMap k K)))
rw₂ : w.IsComplex ∧ IsReal (w.comap (algebraMap k K)) ↔ ¬w.IsReal ∧ ¬IsComplex (w.comap (algebraMap k K))
⊢ IsUnramified k w ↔ w.IsReal ∨ IsComplex (w.comap (algebraMap k K))
have rw₃ : w.IsComplex ∧ IsReal (w.comap (algebraMap k K)) ↔ w.IsComplex ∧ ¬IsComplex (w.comap (algebraMap k K))
Tactic: rw [← not_iff_not, not_isUnramified_iff, not_or,
    not_isReal_iff_isComplex, not_isComplex_iff_isReal]
-- 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
w : InfinitePlace K
rw : ¬IsUnramified k w ↔ ¬(w.IsReal ∨ IsComplex (w.comap (algebraMap k K)))
rw₁ : w.IsComplex ∧ IsReal (w.comap (algebraMap k K)) ↔ ¬(w.IsReal ∨ IsComplex (w.comap (algebraMap k K)))
rw₂ : w.IsComplex ∧ IsReal (w.comap (algebraMap k K)) ↔ ¬w.IsReal ∧ ¬IsComplex (w.comap (algebraMap k K))
rw₃ : w.IsComplex ∧ IsReal (w.comap (algebraMap k K)) ↔ w.IsComplex ∧ ¬IsComplex (w.comap (algebraMap k K))
⊢ IsUnramified k w ↔ w.IsReal ∨ IsComplex (w.comap (algebraMap k K))
have rw₄ : w.IsComplex ∧ IsReal (w.comap (algebraMap k K)) ↔ w.IsComplex ∧ IsReal (w.comap (algebraMap k K))
Tactic: rw [← not_iff_not, not_isUnramified_iff, not_or,
    not_isReal_iff_isComplex, not_isComplex_iff_isReal]
-- 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
w₁ w₂ : InfinitePlace K
h : IsRamified k w₂
⊢ w₁.embedding ≠ conjugate w₂.embedding
have pos : ∀ (h_eq : w₁ = w₂), w₁.embedding ≠ conjugate w₂.embedding
Tactic: by_cases h_eq : w₁ = w₂
-- 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
w₁ w₂ : InfinitePlace K
h : IsRamified k w₂
pos : ∀ (h_eq : w₁ = w₂), w₁.embedding ≠ conjugate w₂.embedding
⊢ w₁.embedding ≠ conjugate w₂.embedding
have neg : ∀ (h_eq : ¬w₁ = w₂), w₁.embedding ≠ conjugate w₂.embedding
Tactic: by_cases h_eq : w₁ = w₂
-- 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
w₁ w₂ : InfinitePlace K
h : IsRamified k w₂
h_eq : w₁ = w₂
⊢ w₁.embedding ≠ conjugate w₂.embedding
have h₁ : ¬ComplexEmbedding.IsReal w₂.embedding ∧ IsReal (w₂.comap (algebraMap k K))
Tactic: rw [isRamified_iff, isComplex_iff] at h
Cleared hypotheses: h, h_eq
-- 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
w₁ w₂ : InfinitePlace K
h : IsRamified k w₂
h_eq : ¬w₁ = w₂
⊢ w₁.embedding ≠ conjugate w₂.embedding
have neg : ∀ (h_eq : w₁.embedding = conjugate w₂.embedding), w₁ = w₂
Tactic: contrapose h_eq
Cleared hypotheses: h_eq
-- 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
w₁ w₂ : InfinitePlace K
h : IsRamified k w₂
h_eq : w₁.embedding = conjugate w₂.embedding
⊢ w₁ = w₂
have neg : mk w₁.embedding = w₂
Tactic: rw [← mk_embedding w₁, h_eq, mk_conjugate_eq, 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
inst_2 : Algebra k K
w₁ w₂ : InfinitePlace K
h : IsRamified k w₂
h_eq : w₁.embedding = conjugate w₂.embedding
neg : mk w₁.embedding = w₂
⊢ w₁ = w₂
have neg₁ : mk (conjugate w₂.embedding) = w₂
Tactic: rw [← mk_embedding w₁, h_eq, mk_conjugate_eq, 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
inst_2 : Algebra k K
w₁ w₂ : InfinitePlace K
h : IsRamified k w₂
h_eq : w₁.embedding = conjugate w₂.embedding
neg : mk w₁.embedding = w₂
neg₁ : mk (conjugate w₂.embedding) = w₂
⊢ w₁ = w₂
have neg₂ : mk w₂.embedding = w₂
Tactic: rw [← mk_embedding w₁, h_eq, mk_conjugate_eq, 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
inst_2 : Algebra k K
w₁ w₂ : InfinitePlace K
h : IsRamified k w₂
h_eq : w₁.embedding = conjugate w₂.embedding
neg : mk w₁.embedding = w₂
neg₁ : mk (conjugate w₂.embedding) = w₂
neg₂ : mk w₂.embedding = w₂
⊢ w₁ = w₂
have neg₃ : w₂ = w₂
Tactic: rw [← mk_embedding w₁, h_eq, mk_conjugate_eq, 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
inst_2 : Algebra k K
w : InfinitePlace K
h : IsRamified k w
⊢ Eq (α := k →+* ℂ) (embedding (w.comap (algebraMap k K))) (w.embedding.comp (algebraMap k K))
have rw : Eq (α := k →+* ℂ) (embedding (w.comap (algebraMap k K))) (embedding (w.comap (algebraMap k K)))
Tactic: rw [← comap_embedding_of_isReal _ (isRamified_iff.1 h).2]
-- 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
w : InfinitePlace K
h : IsRamified k w
⊢ Eq (α := k →+* ℂ) (embedding (w.comap (algebraMap k K))) ((conjugate w.embedding).comp (algebraMap k K))
have rw : Eq (α := k →+* ℂ) (conjugate (embedding (w.comap (algebraMap k K)))) ((conjugate w.embedding).comp (algebraMap k K))
Tactic: rw [← ComplexEmbedding.isReal_iff.1 <| isReal_iff.1 ((isRamified_iff.1 h).2)]
-- 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
φ : K →+* ℂ
⊢ IsRamified k (mk φ) ↔ IsMixed k φ
have refine_1 : ∀ (h : IsRamified k (mk φ)), IsMixed k φ
Tactic: refine ⟨fun h ↦ ?_, fun 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
φ : K →+* ℂ
refine_1 : ∀ (h : IsRamified k (mk φ)), IsMixed k φ
⊢ IsRamified k (mk φ) ↔ IsMixed k φ
have refine_2 : ∀ (h : IsMixed k φ), IsRamified k (mk φ)
Tactic: refine ⟨fun h ↦ ?_, fun 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
φ : K →+* ℂ
h : IsRamified k (mk φ)
⊢ IsMixed k φ
have refine_1 : ∀ (hl : (mk φ).embedding = φ), IsMixed k φ
Tactic: rcases embedding_mk_eq φ with (hl | hr)
-- 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
φ : K →+* ℂ
h : IsRamified k (mk φ)
refine_1 : ∀ (hl : (mk φ).embedding = φ), IsMixed k φ
⊢ IsMixed k φ
have refine_1₁ : ∀ (hr : (mk φ).embedding = conjugate φ), IsMixed k φ
Tactic: rcases embedding_mk_eq φ with (hl | hr)