awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
this : Subgroup.map (Units.map (↑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : 𝓞 ↥K⁺ →* 𝓞 K)) (torsion ↥K⁺) ≤ torsion K
e_a :
  ∀ (x : (𝓞 K)ˣ),
    Membership.mem (γ := Set (𝓞 K)ˣ) (Set.range (ι := Fin (rank K)) (realFundSystem K)) x ↔
      Membership.mem (γ := Set (𝓞 K)ˣ)
        (Set.image (α := (𝓞 ↥K⁺)ˣ) (⇑(Units.map (↑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : 𝓞 ↥K⁺ →* 𝓞 K)) : (a : (𝓞 ↥K⁺)ˣ) → (𝓞 K)ˣ)
          (Set.range (ι := Fin (rank.{u_1} ↥K⁺)) (fundSystem ↥K⁺)))
        x
⊢ Eq (α := Set (𝓞 K)ˣ) (Set.range (ι := Fin (rank K)) (realFundSystem K))
    (Set.image (α := (𝓞 ↥K⁺)ˣ) (⇑(Units.map (↑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : 𝓞 ↥K⁺ →* 𝓞 K)) : (a : (𝓞 ↥K⁺)ˣ) → (𝓞 K)ˣ)
      (Set.range (ι := Fin (rank.{u_1} ↥K⁺)) (fundSystem ↥K⁺)))

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
this : Subgroup.map (Units.map (↑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : 𝓞 ↥K⁺ →* 𝓞 K)) (torsion ↥K⁺) ≤ torsion K
x : (𝓞 K)ˣ
⊢ Membership.mem (γ := Set (𝓞 K)ˣ) (Set.range (ι := Fin (rank K)) (realFundSystem K)) x ↔
    Membership.mem (γ := Set (𝓞 K)ˣ)
      (Set.image (α := (𝓞 ↥K⁺)ˣ) (⇑(Units.map (↑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : 𝓞 ↥K⁺ →* 𝓞 K)) : (a : (𝓞 ↥K⁺)ˣ) → (𝓞 K)ˣ)
        (Set.range (ι := Fin (rank.{u_1} ↥K⁺)) (fundSystem ↥K⁺)))
      x

Tactic:
simp [realFundSystem, Equiv.exists_congr_left (finCongr (units_rank_eq_units_rank K).symm)]

Premises used: NumberField.IsCMField.units_rank_eq_units_rank, Equiv.exists_congr_left, finCongr, NumberField.IsCMField.realFundSystem, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
W₀ : InfinitePlace K := (Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K) w₀
w : InfinitePlace K
rw :
  w = W₀ ↔
    Eq (α := InfinitePlace ↥K⁺)
      ((equivInfinitePlace K : (a : InfinitePlace K) → InfinitePlace ↥K⁺) w : InfinitePlace ↥K⁺)
      (w₀ : InfinitePlace ↥K⁺)
rw₁ rw₂ :
  Eq (α := InfinitePlace ↥K⁺) ((equivInfinitePlace K : (a : InfinitePlace K) → InfinitePlace ↥K⁺) w : InfinitePlace ↥K⁺)
      (w₀ : InfinitePlace ↥K⁺) ↔
    Eq (α := InfinitePlace ↥K⁺)
      ((equivInfinitePlace K : (a : InfinitePlace K) → InfinitePlace ↥K⁺) w : InfinitePlace ↥K⁺)
      (w₀ : InfinitePlace ↥K⁺)
⊢ w ≠ W₀ ↔
    Ne (α := InfinitePlace ↥K⁺)
      ((equivInfinitePlace K : (a : InfinitePlace K) → InfinitePlace ↥K⁺) w : InfinitePlace ↥K⁺)
      (w₀ : InfinitePlace ↥K⁺)

Tactic:
rw [not_iff_not, Equiv.eq_symm_apply]

Premises used: not_iff_not, Equiv.eq_symm_apply
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
W₀ : InfinitePlace K := (Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K) w₀
f : { w : InfinitePlace K // w ≠ W₀ } ≃ { w : InfinitePlace ↥K⁺ // w ≠ w₀ } :=
  Equiv.subtypeEquiv (p := fun (w : InfinitePlace K) ↦ w ≠ W₀) (q := fun (w : InfinitePlace ↥K⁺) ↦ w ≠ w₀)
    (equivInfinitePlace K) ⋯
g : Fin (rank K) ≃ { w : InfinitePlace K // w ≠ W₀ } := Equiv.trans (Equiv.trans (finCongr ⋯) (equivFinRank ↥K⁺)) f.symm
rw :
  HPow.hPow (α := ℝ) 2 (Fintype.card.{u_1} (InfinitePlace ↥K⁺) - 1) =
    HPow.hPow (α := ℝ) 2 (Finset.card.{u_1} (α := { w : InfinitePlace ↥K⁺ // w ≠ w₀ }) Finset.univ)
⊢ HPow.hPow (α := ℝ) 2 (rank K) = |∏ w : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }, 2|

Tactic:
rw [Finset.prod_const, abs_pow, abs_of_pos zero_lt_two, ← units_rank_eq_units_rank K, rank]

Premises used: NumberField.IsCMField.units_rank_eq_units_rank, NumberField.Units.rank, Finset.prod_const, abs_of_pos, abs_pow
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
W₀ : InfinitePlace K := (Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K) w₀
f : { w : InfinitePlace K // w ≠ W₀ } ≃ { w : InfinitePlace ↥K⁺ // w ≠ w₀ } :=
  Equiv.subtypeEquiv (p := fun (w : InfinitePlace K) ↦ w ≠ W₀) (q := fun (w : InfinitePlace ↥K⁺) ↦ w ≠ w₀)
    (equivInfinitePlace K) ⋯
g : Fin (rank K) ≃ { w : InfinitePlace K // w ≠ W₀ } := Equiv.trans (Equiv.trans (finCongr ⋯) (equivFinRank ↥K⁺)) f.symm
⊢ HPow.hPow (α := ℝ) 2 (Fintype.card.{u_1} (InfinitePlace ↥K⁺) - 1) =
    HPow.hPow (α := ℝ) 2 (Finset.card.{u_1} (α := { w : InfinitePlace ↥K⁺ // w ≠ w₀ }) Finset.univ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
W₀ : InfinitePlace K := (Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K) w₀
f : { w : InfinitePlace K // w ≠ W₀ } ≃ { w : InfinitePlace ↥K⁺ // w ≠ w₀ } :=
  Equiv.subtypeEquiv (p := fun (w : InfinitePlace K) ↦ w ≠ W₀) (q := fun (w : InfinitePlace ↥K⁺) ↦ w ≠ w₀)
    (equivInfinitePlace K) ⋯
g : Fin (rank K) ≃ { w : InfinitePlace K // w ≠ W₀ } := Equiv.trans (Equiv.trans (finCongr ⋯) (equivFinRank ↥K⁺)) f.symm
rw : regOfFamily (realFundSystem K) = |∏ w : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }, 2| * regulator.{u_1} ↥K⁺
⊢ regOfFamily (realFundSystem K) = HPow.hPow (α := ℝ) 2 (rank K) * regulator.{u_1} ↥K⁺

Tactic:
rw [show (2 : ℝ) ^ rank K = |∏ w : {w : InfinitePlace K⁺ // w ≠ w₀}, 2| by
    rw [Finset.prod_const, abs_pow, abs_of_pos zero_lt_two, ← units_rank_eq_units_rank K, rank]
    simp]
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
W₀ : InfinitePlace K := (Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K) w₀
f : { w : InfinitePlace K // w ≠ W₀ } ≃ { w : InfinitePlace ↥K⁺ // w ≠ w₀ } :=
  Equiv.subtypeEquiv (p := fun (w : InfinitePlace K) ↦ w ≠ W₀) (q := fun (w : InfinitePlace ↥K⁺) ↦ w ≠ w₀)
    (equivInfinitePlace K) ⋯
g : Fin (rank K) ≃ { w : InfinitePlace K // w ≠ W₀ } := Equiv.trans (Equiv.trans (finCongr ⋯) (equivFinRank ↥K⁺)) f.symm
i w : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }
⊢ Eq (α := InfinitePlace K)
    ((↑((f.symm : (a : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }) → { w : InfinitePlace K // w ≠ W₀ }) w) : InfinitePlace K) :
      InfinitePlace K)
    ((Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K) (↑w : InfinitePlace ↥K⁺) :
      InfinitePlace K)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
W₀ : InfinitePlace K := (Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K) w₀
f : { w : InfinitePlace K // w ≠ W₀ } ≃ { w : InfinitePlace ↥K⁺ // w ≠ w₀ } :=
  Equiv.subtypeEquiv (p := fun (w : InfinitePlace K) ↦ w ≠ W₀) (q := fun (w : InfinitePlace ↥K⁺) ↦ w ≠ w₀)
    (equivInfinitePlace K) ⋯
g : Fin (rank K) ≃ { w : InfinitePlace K // w ≠ W₀ } := Equiv.trans (Equiv.trans (finCongr ⋯) (equivFinRank ↥K⁺)) f.symm
i w : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }
⊢ Eq (α := K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
        (↑(realFundSystem K
              ((g.symm : (a : { w : InfinitePlace K // w ≠ W₀ }) → Fin (rank K))
                ((f.symm : (a : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }) → { w : InfinitePlace K // w ≠ W₀ }) i))) :
          𝓞 K) :
      K)
    ((algebraMap (↥K⁺) K : (a : ↥K⁺) → K)
        (↑(↑(fundSystem (↥K⁺)
                  ((finCongr ⋯ : (a : Fin (rank K)) → Fin (rank ↥K⁺))
                    ((g.symm : (a : { w : InfinitePlace K // w ≠ W₀ }) → Fin (rank K))
                      ((f.symm : (a : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }) → { w : InfinitePlace K // w ≠ W₀ }) i)))) :
              𝓞 ↥K⁺) :
          ↥K⁺) :
      K)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
W₀ : InfinitePlace K := (Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K) w₀
f : { w : InfinitePlace K // w ≠ W₀ } ≃ { w : InfinitePlace ↥K⁺ // w ≠ w₀ } :=
  Equiv.subtypeEquiv (p := fun (w : InfinitePlace K) ↦ w ≠ W₀) (q := fun (w : InfinitePlace ↥K⁺) ↦ w ≠ w₀)
    (equivInfinitePlace K) ⋯
g : Fin (rank K) ≃ { w : InfinitePlace K // w ≠ W₀ } := Equiv.trans (Equiv.trans (finCongr ⋯) (equivFinRank ↥K⁺)) f.symm
i w : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }
⊢ (↑(mult.{u_1} (K := K)
            ((Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K)
              (↑w : InfinitePlace ↥K⁺))) :
        ℝ) *
      Real.log
        (((↑w : InfinitePlace ↥K⁺) : (a : ↥K⁺) → ℝ)
          (↑(↑(fundSystem (↥K⁺)
                    ((finCongr ⋯ : (a : Fin (rank K)) → Fin (rank ↥K⁺))
                      ((g.symm : (a : { w : InfinitePlace K // w ≠ W₀ }) → Fin (rank K))
                        ((f.symm : (a : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }) → { w : InfinitePlace K // w ≠ W₀ })
                          i)))) :
                𝓞 ↥K⁺) :
            ↥K⁺)) =
    HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ)
      ((Matrix.of :
            (a : { w : InfinitePlace ↥K⁺ // w ≠ w₀ } → { w : InfinitePlace ↥K⁺ // w ≠ w₀ } → ℝ) →
              Matrix { w : InfinitePlace ↥K⁺ // w ≠ w₀ } { w : InfinitePlace ↥K⁺ // w ≠ w₀ } ℝ)
          (fun (i : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }) ↦
            (logEmbedding ↥K⁺ : (a : Additive (𝓞 ↥K⁺)ˣ) → logSpace ↥K⁺)
              ((Additive.ofMul : (a : (𝓞 ↥K⁺)ˣ) → Additive (𝓞 ↥K⁺)ˣ)
                  (fundSystem (↥K⁺)
                    (((Equiv.symm (equivFinRank ↥K⁺) : { w : InfinitePlace ↥K⁺ // w ≠ w₀ } ≃ Fin (rank.{u_1} ↥K⁺)) :
                        (a : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }) → Fin (rank ↥K⁺))
                      i)) :
                Additive (𝓞 ↥K⁺)ˣ))
          i w :
        ℝ)

Tactic:
simp [f, g]
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
⊢ HPow.hPow (α := ℝ) 2 (rank K) ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
rw :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) * (↑(Subgroup.index (G := (𝓞 K)ˣ) (realUnits K ⊔ torsion K)) : ℝ)⁻¹
rw₁ :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) *
      (↑(Subgroup.index (G := (𝓞 K)ˣ)
              (Subgroup.closure (Set.range (ι := Fin (rank K)) (realFundSystem K)) ⊔ torsion K)) :
          ℝ)⁻¹
rw₂ :
  regulator K / regulator.{u_1} ↥K⁺ = HPow.hPow (α := ℝ) 2 (rank K) * (regOfFamily (realFundSystem K) / regulator K)⁻¹
rw₃ :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) * (HPow.hPow (α := ℝ) 2 (rank K) * regulator.{u_1} ↥K⁺ / regulator K)⁻¹
rw₄ :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) * (regulator K / (HPow.hPow (α := ℝ) 2 (rank K) * regulator.{u_1} ↥K⁺))
rw₅ :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) * regulator K / (HPow.hPow (α := ℝ) 2 (rank K) * regulator.{u_1} ↥K⁺)
rw₆ :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) / HPow.hPow (α := ℝ) 2 (rank K) * (regulator K / regulator.{u_1} ↥K⁺)
rw₇ : regulator K / regulator.{u_1} ↥K⁺ = 1 * (regulator K / regulator.{u_1} ↥K⁺)
rw₈ rw₉ : regulator K / regulator.{u_1} ↥K⁺ = regulator K / regulator.{u_1} ↥K⁺
⊢ regulator K / regulator.{u_1} ↥K⁺ = HPow.hPow (α := ℝ) 2 (rank K) * (↑(indexRealUnits K) : ℝ)⁻¹

Tactic:
rw [indexRealUnits, ← closure_realFundSystem_sup_torsion, ← regOfFamily_div_regulator
    (realFundSystem K), regOfFamily_realFunSystem, inv_div, ← mul_div_assoc, mul_div_mul_comm,
    div_self (by positivity), one_mul]

Premises used: mul_div_assoc, NumberField.IsCMField.realFundSystem, NumberField.Units.regOfFamily_div_regulator, NumberField.IsCMField.closure_realFundSystem_sup_torsion, NumberField.IsCMField.indexRealUnits, inv_div, mul_div_mul_comm, one_mul, div_self, NumberField.IsCMField.regOfFamily_realFunSystem
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
E : Subfield K
inst_4 : IsTotallyReal.{u_2} ↥E
inst_5 : IsQuadraticExtension (↥E) K
⊢ E = maximalRealSubfield K

Tactic:
le_antisymm (IsTotallyReal.le_maximalRealSubfield E) ?_

Premises used: le_antisymm, NumberField.IsTotallyReal.le_maximalRealSubfield
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
E : Subfield K
inst_4 : IsTotallyReal.{u_2} ↥E
inst_5 : IsQuadraticExtension (↥E) K
refine : maximalRealSubfield K ≤ E
⊢ E = maximalRealSubfield K

Tactic:
refine le_antisymm (IsTotallyReal.le_maximalRealSubfield E) ?_

Premises used: le_antisymm, NumberField.IsTotallyReal.le_maximalRealSubfield
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
E : Subfield K
inst_4 : IsTotallyReal.{u_2} ↥E
inst_5 : IsQuadraticExtension (↥E) K
by_contra! : ∀ (h : ¬maximalRealSubfield K ≤ E), False
⊢ maximalRealSubfield K ≤ E

Tactic:
by_contra! h
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
E : Subfield K
inst_4 : IsTotallyReal.{u_2} ↥E
inst_5 : IsQuadraticExtension (↥E) K
h : ¬maximalRealSubfield K ≤ E
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
refine_2 : ∀ (this : L = ⊤), E ⊔ maximalRealSubfield K = ⊤
refine_1 : ¬L = ⊥
⊢ E ⊔ maximalRealSubfield K = ⊤

Tactic:
have := ((IntermediateField.isSimpleOrder_of_finrank_prime E K
      (IsQuadraticExtension.finrank_eq_two E K ▸ Nat.prime_two)).eq_bot_or_eq_top L).resolve_left ?_
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
E : Subfield K
inst_4 : IsTotallyReal.{u_2} ↥E
inst_5 : IsQuadraticExtension (↥E) K
h : ¬maximalRealSubfield K ≤ E
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
this : L = ⊤
⊢ E ⊔ maximalRealSubfield K = ⊤

Tactic:
simpa [L] using congr_arg IntermediateField.toSubfield this

Premises used: congr_arg, IntermediateField.toSubfield
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
E : Subfield K
inst_4 : IsTotallyReal.{u_2} ↥E
inst_5 : IsQuadraticExtension (↥E) K
h : ¬maximalRealSubfield K ≤ E
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
refine_1 : ∀ (h : L = ⊥), maximalRealSubfield K ≤ E
⊢ ¬L = ⊥

Tactic:
contrapose h
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
E : Subfield K
inst_4 : IsTotallyReal.{u_2} ↥E
inst_5 : IsQuadraticExtension (↥E) K
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
h : L = ⊥
⊢ (↑(E ⊔ maximalRealSubfield K) : Set K) = (↑⊥ : Set K)

Tactic:
rw [← SetLike.coe_set_eq, Subfield.coe_toIntermediateField] at h

Premises used: Subfield.coe_toIntermediateField, SetLike.coe_set_eq
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
E : Subfield K
inst_4 : IsTotallyReal.{u_2} ↥E
inst_5 : IsQuadraticExtension (↥E) K
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
h : (↑(E ⊔ maximalRealSubfield K) : Set K) = (↑⊥ : Set K)
refine_1 : Set.range (ι := ↥E) (⇑(algebraMap (↥E) K) : (a : ↥E) → K) = (↑E : Set K)
⊢ maximalRealSubfield K ≤ E

Tactic:
rw [← sup_eq_left, ← SetLike.coe_set_eq, h, IntermediateField.coe_bot]

Premises used: IntermediateField.coe_bot, sup_eq_left, SetLike.coe_set_eq
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
E : Subfield K
inst_4 : IsTotallyReal.{u_2} ↥E
inst_5 : IsQuadraticExtension (↥E) K
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
h : (↑(E ⊔ maximalRealSubfield K) : Set K) = (↑⊥ : Set K)
⊢ Set.range (ι := ↥E) (⇑(algebraMap (↥E) K) : (a : ↥E) → K) = (↑E : Set K)

Tactic:
aesop
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
E : Subfield K
inst_4 : IsTotallyReal.{u_2} ↥E
inst_5 : IsQuadraticExtension (↥E) K
h : ¬maximalRealSubfield K ≤ E
⊢ E ⊔ maximalRealSubfield K = ⊤

Tactic:
have h' : E ⊔ (maximalRealSubfield K) = ⊤ := by
    let L : IntermediateField E K := (E ⊔ (maximalRealSubfield K)).toIntermediateField
      (fun x ↦ (le_sup_left (a := E)) x.prop)
    have := ((IntermediateField.isSimpleOrder_of_finrank_prime E K
      (IsQuadraticExtension.finrank_eq_two E K ▸ Nat.prime_two)).eq_bot_or_eq_top L).resolve_left ?_
    · simpa [L] using congr_arg IntermediateField.toSubfield this
    · contrapose h
      rw [← SetLike.coe_set_eq, Subfield.coe_toIntermediateField] at h
      rw [← sup_eq_left, ← SetLike.coe_set_eq, h, IntermediateField.coe_bot]
      aesop
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
E : Subfield K
inst_4 : IsTotallyReal.{u_2} ↥E
inst_5 : IsQuadraticExtension (↥E) K
h : ¬maximalRealSubfield K ≤ E
h' : E ⊔ maximalRealSubfield K = ⊤
⊢ Algebra.IsAlgebraic (↥(maximalRealSubfield K)) K

Tactic:
have : Algebra.IsAlgebraic (maximalRealSubfield K) K :=
    Algebra.IsAlgebraic.tower_top (K := ℚ) (maximalRealSubfield K)
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
E : Subfield K
inst_4 : IsTotallyReal.{u_2} ↥E
inst_5 : IsQuadraticExtension (↥E) K
h : ¬maximalRealSubfield K ≤ E
h' : E ⊔ maximalRealSubfield K = ⊤
this : Algebra.IsAlgebraic (↥(maximalRealSubfield K)) K
⊢ IsTotallyReal K

Tactic:
have : IsTotallyReal K := (h' ▸ isTotallyReal_sup).ofRingEquiv Subring.topEquiv
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
E : Subfield K
inst_4 : IsTotallyReal.{u_2} ↥E
inst_5 : IsQuadraticExtension (↥E) K
h : ¬maximalRealSubfield K ≤ E
h' : E ⊔ maximalRealSubfield K = ⊤
this_1 : Algebra.IsAlgebraic (↥(maximalRealSubfield K)) K
this : IsTotallyReal K
obtain : ∀ (w : InfinitePlace K), False
⊢ False

Tactic:
obtain w : InfinitePlace K := Classical.choice (inferInstance : Nonempty _)

Premises used: Classical.choice, inferInstance, NumberField.InfinitePlace
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
E : Subfield K
inst_4 : IsTotallyReal.{u_2} ↥E
inst_5 : IsQuadraticExtension (↥E) K
h : ¬maximalRealSubfield K ≤ E
h' : E ⊔ maximalRealSubfield K = ⊤
this_1 : Algebra.IsAlgebraic (↥(maximalRealSubfield K)) K
this : IsTotallyReal K
w : InfinitePlace K
⊢ False

Tactic:
(not_isReal_iff_isComplex.mpr (IsTotallyComplex.isComplex w)) (IsTotallyReal.isReal w)

Premises used: Iff.mpr, NumberField.IsTotallyComplex.isComplex, NumberField.InfinitePlace.not_isReal_iff_isComplex, NumberField.IsTotallyReal.isReal
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
E : Subfield K
inst_4 : IsTotallyReal.{u_2} ↥E
inst_5 : IsQuadraticExtension (↥E) K
h : ¬maximalRealSubfield K ≤ E
h' : E ⊔ maximalRealSubfield K = ⊤
this_1 : Algebra.IsAlgebraic (↥(maximalRealSubfield K)) K
this : IsTotallyReal K
w : InfinitePlace K
⊢ False

Tactic:
exact (not_isReal_iff_isComplex.mpr (IsTotallyComplex.isComplex w)) (IsTotallyReal.isReal w)

Premises used: Iff.mpr, NumberField.IsTotallyComplex.isComplex, NumberField.InfinitePlace.not_isReal_iff_isComplex, NumberField.IsTotallyReal.isReal
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : IsTotallyReal F
inst_2 : Field K
inst_3 : CharZero K
inst_4 : Algebra.IsIntegral ℚ K
inst_5 : IsTotallyComplex K
inst_6 : Algebra F K
inst_7 : IsQuadraticExtension F K
⊢ IsTotallyReal.{u_2} ↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K))

Tactic:
have := IsTotallyReal.ofRingEquiv (algebraMap F K).rangeRestrictFieldEquiv
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : IsTotallyReal F
inst_2 : Field K
inst_3 : CharZero K
inst_4 : Algebra.IsIntegral ℚ K
inst_5 : IsTotallyComplex K
inst_6 : Algebra F K
inst_7 : IsQuadraticExtension F K
this : IsTotallyReal.{u_2} ↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K))
a :
  ∀ (x : ↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K))),
    Eq (α := K)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap F K)
              (RingEquiv.toRingHom (RingEquiv.symm (RingHom.rangeRestrictFieldEquiv (algebraMap F K)))) :
            (a : ↥(algebraMap F K).fieldRange) → K)
          x :
        K)
      ((RingHom.comp (RingEquiv.toRingHom (RingEquiv.refl K))
              (algebraMap (↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K))) K) :
            (a : ↥(algebraMap F K).fieldRange) → K)
          x :
        K)
⊢ Eq (α := ↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K)) →+* K)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap F K)
      (RingEquiv.toRingHom (RingEquiv.symm (RingHom.rangeRestrictFieldEquiv (algebraMap F K)))))
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.refl K))
      (algebraMap (↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K))) K))

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : IsTotallyReal F
inst_2 : Field K
inst_3 : CharZero K
inst_4 : Algebra.IsIntegral ℚ K
inst_5 : IsTotallyComplex K
inst_6 : Algebra F K
inst_7 : IsQuadraticExtension F K
this : IsTotallyReal.{u_2} ↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K))
x : ↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K))
a :
  (↑x : K) =
    (algebraMap (↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K))) K : (a : ↥(algebraMap F K).fieldRange) → K)
      x
⊢ Eq (α := K)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap F K)
            (RingEquiv.toRingHom (RingEquiv.symm (RingHom.rangeRestrictFieldEquiv (algebraMap F K)))) :
          (a : ↥(algebraMap F K).fieldRange) → K)
        x :
      K)
    ((RingHom.comp (RingEquiv.toRingHom (RingEquiv.refl K))
            (algebraMap (↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K))) K) :
          (a : ↥(algebraMap F K).fieldRange) → K)
        x :
      K)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : IsTotallyReal F
inst_2 : Field K
inst_3 : CharZero K
inst_4 : Algebra.IsIntegral ℚ K
inst_5 : IsTotallyComplex K
inst_6 : Algebra F K
inst_7 : IsQuadraticExtension F K
this : IsTotallyReal.{u_2} ↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K))
x : ↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K))
⊢ (↑x : K) =
    (algebraMap (↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K))) K : (a : ↥(algebraMap F K).fieldRange) → K)
      x

Tactic:
rfl