awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
L : Type u_3
inst : Field L
K₁ : Type u_4
K₂ : Type u_5
inst_1 : Field K₁
inst_2 : NumberField K₁
inst_3 : Field K₂
inst_4 : NumberField K₂
inst_5 : Algebra K₁ L
inst_6 : Algebra K₂ L
u v : ℤ
h : u * discr K₁ + v * discr K₂ = 1
⊢ Membership.mem (γ := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 K₁) (F := RingHom.{u_4, u_3} (𝓞 K₁) (𝓞 L)) (algebraMap (𝓞 K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 K₁)))
    ((algebraMap (𝓞 K₁) (𝓞 L) : (a : 𝓞 K₁) → 𝓞 L) (↑(discr K₁) : 𝓞 K₁))

Tactic:
exact Ideal.mem_map_of_mem (algebraMap (𝓞 K₁) (𝓞 L)) <| discr_mem_differentIdeal _ _

Premises used: Algebra.algebraMap, Ideal.mem_map_of_mem, NumberField.discr_mem_differentIdeal, NumberField.RingOfIntegers
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
L : Type u_3
inst : Field L
K₁ : Type u_4
K₂ : Type u_5
inst_1 : Field K₁
inst_2 : NumberField K₁
inst_3 : Field K₂
inst_4 : NumberField K₂
inst_5 : Algebra K₁ L
inst_6 : Algebra K₂ L
u v : ℤ
h : u * discr K₁ + v * discr K₂ = 1
refine_2 :
  Membership.mem (γ := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 K₂) (F := RingHom.{u_5, u_3} (𝓞 K₂) (𝓞 L)) (algebraMap (𝓞 K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 K₂)))
    (↑(discr K₂) : 𝓞 L)
⊢ Membership.mem (γ := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 K₂) (F := RingHom.{u_5, u_3} (𝓞 K₂) (𝓞 L)) (algebraMap (𝓞 K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 K₂)))
    (HMul.hMul (α := 𝓞 L) (↑v : 𝓞 L) (↑(discr K₂) : 𝓞 L))

Tactic:
apply Ideal.mul_mem_left

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
L : Type u_3
inst : Field L
K₁ : Type u_4
K₂ : Type u_5
inst_1 : Field K₁
inst_2 : NumberField K₁
inst_3 : Field K₂
inst_4 : NumberField K₂
inst_5 : Algebra K₁ L
inst_6 : Algebra K₂ L
u v : ℤ
h : u * discr K₁ + v * discr K₂ = 1
refine_2 :
  Membership.mem (γ := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 K₂) (F := RingHom.{u_5, u_3} (𝓞 K₂) (𝓞 L)) (algebraMap (𝓞 K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 K₂)))
    ((algebraMap (𝓞 K₂) (𝓞 L) : (a : 𝓞 K₂) → 𝓞 L) (↑(discr K₂) : 𝓞 K₂))
⊢ Membership.mem (γ := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 K₂) (F := RingHom.{u_5, u_3} (𝓞 K₂) (𝓞 L)) (algebraMap (𝓞 K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 K₂)))
    (↑(discr K₂) : 𝓞 L)

Tactic:
rw [← map_intCast (algebraMap (𝓞 K₂) (𝓞 L))]

Premises used: Algebra.algebraMap, map_intCast, NumberField.RingOfIntegers
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
L : Type u_3
inst : Field L
K₁ : Type u_4
K₂ : Type u_5
inst_1 : Field K₁
inst_2 : NumberField K₁
inst_3 : Field K₂
inst_4 : NumberField K₂
inst_5 : Algebra K₁ L
inst_6 : Algebra K₂ L
u v : ℤ
h : u * discr K₁ + v * discr K₂ = 1
⊢ Membership.mem (γ := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 K₂) (F := RingHom.{u_5, u_3} (𝓞 K₂) (𝓞 L)) (algebraMap (𝓞 K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 K₂)))
    ((algebraMap (𝓞 K₂) (𝓞 L) : (a : 𝓞 K₂) → 𝓞 L) (↑(discr K₂) : 𝓞 K₂))

Tactic:
Ideal.mem_map_of_mem (algebraMap (𝓞 K₂) (𝓞 L)) <| discr_mem_differentIdeal _ _

Premises used: Algebra.algebraMap, Ideal.mem_map_of_mem, NumberField.discr_mem_differentIdeal, NumberField.RingOfIntegers
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
L : Type u_3
inst : Field L
K₁ : Type u_4
K₂ : Type u_5
inst_1 : Field K₁
inst_2 : NumberField K₁
inst_3 : Field K₂
inst_4 : NumberField K₂
inst_5 : Algebra K₁ L
inst_6 : Algebra K₂ L
u v : ℤ
h : u * discr K₁ + v * discr K₂ = 1
⊢ Membership.mem (γ := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 K₂) (F := RingHom.{u_5, u_3} (𝓞 K₂) (𝓞 L)) (algebraMap (𝓞 K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 K₂)))
    ((algebraMap (𝓞 K₂) (𝓞 L) : (a : 𝓞 K₂) → 𝓞 L) (↑(discr K₂) : 𝓞 K₂))

Tactic:
exact Ideal.mem_map_of_mem (algebraMap (𝓞 K₂) (𝓞 L)) <| discr_mem_differentIdeal _ _

Premises used: Algebra.algebraMap, Ideal.mem_map_of_mem, NumberField.discr_mem_differentIdeal, NumberField.RingOfIntegers
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
L : Type u_3
inst : Field L
K₁ : Type u_4
K₂ : Type u_5
inst_1 : Field K₁
inst_2 : NumberField K₁
inst_3 : Field K₂
inst_4 : NumberField K₂
inst_5 : Algebra K₁ L
inst_6 : Algebra K₂ L
u v : ℤ
h : u * discr K₁ + v * discr K₂ = 1
refine_3 : (↑(u * discr K₁) : 𝓞 L) + HMul.hMul (α := 𝓞 L) (↑v : 𝓞 L) (↑(discr K₂) : 𝓞 L) = 1
refine_3₁ : HAdd.hAdd (α := 𝓞 L) (↑(u * discr K₁) : 𝓞 L) (↑(v * discr K₂) : 𝓞 L) = 1
refine_3₂ : Eq.{u_3 + 1} (α := 𝓞 L) (↑(u * discr K₁ + v * discr K₂) : 𝓞 L) 1
refine_3₃ : Eq.{u_3 + 1} (α := 𝓞 L) (↑1 : 𝓞 L) 1
refine_3₄ refine_3₅ : Eq.{u_3 + 1} (α := 𝓞 L) 1 1
⊢ HMul.hMul (α := 𝓞 L) (↑u : 𝓞 L) (↑(discr K₁) : 𝓞 L) + HMul.hMul (α := 𝓞 L) (↑v : 𝓞 L) (↑(discr K₂) : 𝓞 L) = 1

Tactic:
rw [← Int.cast_mul, ← Int.cast_mul, ← Int.cast_add, h, Int.cast_one]

Premises used: Int.cast_add, Int.cast_mul, Int.cast_one
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
L : Type u_3
inst_2 : Field L
inst_3 : NumberField L
inst_4 : Algebra K L
suffices : discr K ^ finrank K L ∣ discr L
⊢ discr K ∣ discr L

Tactic:
suffices discr K ^ Module.finrank K L ∣ discr L from
    dvd_trans (dvd_pow_self _ (Nat.ne_zero_of_lt Module.finrank_pos)) this
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
L : Type u_3
inst_2 : Field L
inst_3 : NumberField L
inst_4 : Algebra K L
rw :
  discr K ^ finrank K L ∣
    discr K ^ finrank K L *
      ((↑((Ideal.absNorm : (a : Ideal (𝓞 L)) → ℕ) (differentIdeal.{u_1, u_3} (𝓞 K) (𝓞 L))) : ℤ) *
        (discr K).sign ^ finrank K L)
⊢ discr K ^ finrank K L ∣ discr L

Tactic:
rw [← Int.dvd_natAbs, natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow K (𝓞 K) L (𝓞 L),
    Nat.cast_mul, Nat.cast_pow, ← Int.mul_sign_self, mul_pow, ← mul_assoc,
    mul_comm _ (discr K ^ _), mul_assoc]

Premises used: Int.dvd_natAbs, mul_assoc, Int.mul_sign_self, NumberField.natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow, Nat.cast_mul, HPow.hPow, mul_comm, NumberField.discr, Nat.cast_pow, NumberField.RingOfIntegers, mul_pow
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
L : Type u_3
inst_2 : Field L
inst_3 : NumberField L
inst_4 : Algebra K L
⊢ discr K ^ finrank K L ∣
    discr K ^ finrank K L *
      ((↑((Ideal.absNorm : (a : Ideal (𝓞 L)) → ℕ) (differentIdeal.{u_1, u_3} (𝓞 K) (𝓞 L))) : ℤ) *
        (discr K).sign ^ finrank K L)

Tactic:
Int.dvd_mul_right _ _

Premises used: Int.dvd_mul_right
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
L : Type u_3
inst_2 : Field L
inst_3 : NumberField L
inst_4 : Algebra K L
⊢ discr K ^ finrank K L ∣
    discr K ^ finrank K L *
      ((↑((Ideal.absNorm : (a : Ideal (𝓞 L)) → ℕ) (differentIdeal.{u_1, u_3} (𝓞 K) (𝓞 L))) : ℤ) *
        (discr K).sign ^ finrank K L)

Tactic:
exact Int.dvd_mul_right _ _

Premises used: Int.dvd_mul_right
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
L : Type u_3
inst : Field L
inst_1 : NumberField L
K₁ K₂ : IntermediateField ℚ L
inst_2 : IsGalois.{0, u_3} ℚ ↥K₁
h : IsCoprime (discr.{u_3} ↥K₁) (discr.{u_3} ↥K₂)
h₁ : K₁ ⊓ K₂ = ⊥
⊢ K₁.LinearDisjoint ↥K₂

Tactic:
apply IntermediateField.LinearDisjoint.of_inf_eq_bot

Premises used: IntermediateField.LinearDisjoint.of_inf_eq_bot
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
L : Type u_3
inst : Field L
inst_1 : NumberField L
K₁ K₂ : IntermediateField ℚ L
inst_2 : IsGalois.{0, u_3} ℚ ↥K₁
h : IsCoprime (discr.{u_3} ↥K₁) (discr.{u_3} ↥K₂)
this : IsUnit (discr.{u_3} ↥(K₁ ⊓ K₂))
contrapose! : ∀ (this : K₁ ⊓ K₂ ≠ ⊥), ¬IsUnit (discr.{u_3} ↥(K₁ ⊓ K₂))
⊢ K₁ ⊓ K₂ = ⊥

Tactic:
contrapose! this
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
L : Type u_3
inst : Field L
inst_1 : NumberField L
K₁ K₂ : IntermediateField ℚ L
inst_2 : IsGalois.{0, u_3} ℚ ↥K₁
h : IsCoprime (discr.{u_3} ↥K₁) (discr.{u_3} ↥K₂)
this : K₁ ⊓ K₂ ≠ ⊥
⊢ 1 < finrank.{0, u_3} ℚ ↥(K₁ ⊓ K₂)

Tactic:
Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨Module.finrank_pos.ne', ?_⟩

Premises used: Iff.mpr, LT.lt.ne', And.intro, Nat.one_lt_iff_ne_zero_and_ne_one, Module.finrank_pos
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
L : Type u_3
inst : Field L
inst_1 : NumberField L
K₁ K₂ : IntermediateField ℚ L
inst_2 : IsGalois.{0, u_3} ℚ ↥K₁
h : IsCoprime (discr.{u_3} ↥K₁) (discr.{u_3} ↥K₂)
this : K₁ ⊓ K₂ ≠ ⊥
refine : finrank.{0, u_3} ℚ ↥(K₁ ⊓ K₂) ≠ 1
⊢ 1 < finrank.{0, u_3} ℚ ↥(K₁ ⊓ K₂)

Tactic:
refine Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨Module.finrank_pos.ne', ?_⟩

Premises used: Iff.mpr, LT.lt.ne', And.intro, Nat.one_lt_iff_ne_zero_and_ne_one, Module.finrank_pos
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
L : Type u_3
inst : Field L
inst_1 : NumberField L
K₁ K₂ : IntermediateField ℚ L
inst_2 : IsGalois.{0, u_3} ℚ ↥K₁
h : IsCoprime (discr.{u_3} ↥K₁) (discr.{u_3} ↥K₂)
this : K₁ ⊓ K₂ ≠ ⊥
rwa : ∀ (this : ¬K₁ ⊓ K₂ = ⊥), finrank.{0, u_3} ℚ ↥(K₁ ⊓ K₂) ≠ 1
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : ¬finrank.{0, u_3} ℚ ↥(K₁ ⊓ K₂) = 1), finrank.{0, u_3} ℚ ↥(K₁ ⊓ K₂) ≠ 1
⊢ finrank.{0, u_3} ℚ ↥(K₁ ⊓ K₂) ≠ 1

Tactic:
rwa [ne_eq, ← IntermediateField.finrank_eq_one_iff] at this

Premises used: IntermediateField.finrank_eq_one_iff, ne_eq
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
L : Type u_3
inst : Field L
inst_1 : NumberField L
K₁ K₂ : IntermediateField ℚ L
inst_2 : IsGalois.{0, u_3} ℚ ↥K₁
h : IsCoprime (discr.{u_3} ↥K₁) (discr.{u_3} ↥K₂)
this : K₁ ⊓ K₂ ≠ ⊥
⊢ 1 < finrank.{0, u_3} ℚ ↥(K₁ ⊓ K₂)

Tactic:
have : 1 < Module.finrank ℚ ↥(K₁ ⊓ K₂) := by
      refine Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨Module.finrank_pos.ne', ?_⟩
      rwa [ne_eq, ← IntermediateField.finrank_eq_one_iff] at this
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
L : Type u_3
inst : Field L
inst_1 : NumberField L
K₁ K₂ : IntermediateField ℚ L
inst_2 : IsGalois.{0, u_3} ℚ ↥K₁
h : IsCoprime (discr.{u_3} ↥K₁) (discr.{u_3} ↥K₂)
this_1 : K₁ ⊓ K₂ ≠ ⊥
this : 1 < finrank.{0, u_3} ℚ ↥(K₁ ⊓ K₂)
linarith :
  |discr.{u_3} ↥(K₁ ⊓ K₂)| = 1 →
    HMul.hMul (α := ℤ) 2 (-1) + (|discr.{u_3} ↥(K₁ ⊓ K₂)| - 1) + (HAdd.hAdd (α := ℤ) 2 1 - |discr.{u_3} ↥(K₁ ⊓ K₂)|) = 0
linarith₁ : |discr.{u_3} ↥(K₁ ⊓ K₂)| = 1 → GT.gt (α := ℤ) 2 0
⊢ ¬|discr.{u_3} ↥(K₁ ⊓ K₂)| = 1

Tactic:
linarith [abs_discr_gt_two this]

Premises used: NumberField.abs_discr_gt_two
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
L : Type u_3
inst : Field L
inst_1 : NumberField L
K₁ K₂ : IntermediateField ℚ L
inst_2 : IsGalois.{0, u_3} ℚ ↥K₁
h : IsCoprime (discr.{u_3} ↥K₁) (discr.{u_3} ↥K₂)
this_1 : K₁ ⊓ K₂ ≠ ⊥
this : 1 < finrank.{0, u_3} ℚ ↥(K₁ ⊓ K₂)
⊢ ¬IsUnit (discr.{u_3} ↥(K₁ ⊓ K₂))

Tactic:
exact Int.isUnit_iff_abs_eq.not.mpr <| by linarith [abs_discr_gt_two this]

Premises used: Iff.mpr, Iff.not, Int.isUnit_iff_abs_eq
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
L : Type u_3
inst : Field L
inst_1 : NumberField L
K₁ K₂ : IntermediateField ℚ L
inst_2 : IsGalois.{0, u_3} ℚ ↥K₁
h : IsCoprime (discr.{u_3} ↥K₁) (discr.{u_3} ↥K₂)
h₁ : IsUnit (discr.{u_3} ↥(K₁ ⊓ K₂))
⊢ K₁ ⊓ K₂ = ⊥

Tactic:
suffices IsUnit (discr ↥(K₁ ⊓ K₂)) by
    contrapose! this
    have : 1 < Module.finrank ℚ ↥(K₁ ⊓ K₂) := by
      refine Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨Module.finrank_pos.ne', ?_⟩
      rwa [ne_eq, ← IntermediateField.finrank_eq_one_iff] at this
    exact Int.isUnit_iff_abs_eq.not.mpr <| by linarith [abs_discr_gt_two this]
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
L : Type u_3
inst : Field L
inst_1 : NumberField L
K₁ K₂ : IntermediateField ℚ L
inst_2 : IsGalois.{0, u_3} ℚ ↥K₁
h : IsCoprime (discr.{u_3} ↥K₁) (discr.{u_3} ↥K₂)
⊢ IsUnit (discr.{u_3} ↥(K₁ ⊓ K₂))

Tactic:
h.isUnit_of_dvd' (NumberField.discr_dvd_discr _ _) (NumberField.discr_dvd_discr _ _)

Premises used: IsCoprime.isUnit_of_dvd', NumberField.discr_dvd_discr
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
L : Type u_3
inst : Field L
inst_1 : NumberField L
K₁ K₂ : IntermediateField ℚ L
inst_2 : IsGalois.{0, u_3} ℚ ↥K₁
h : IsCoprime (discr.{u_3} ↥K₁) (discr.{u_3} ↥K₂)
⊢ IsUnit (discr.{u_3} ↥(K₁ ⊓ K₂))

Tactic:
exact h.isUnit_of_dvd' (NumberField.discr_dvd_discr _ _) (NumberField.discr_dvd_discr _ _)

Premises used: IsCoprime.isUnit_of_dvd', NumberField.discr_dvd_discr
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
L : Type u_3
inst : Field L
inst_1 : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime.{u_3} (R := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 ↥K₁) (F := 𝓞 ↥K₁ →+* 𝓞 L) (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (R := 𝓞 ↥K₂) (F := 𝓞 ↥K₂ →+* 𝓞 L) (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
⊢ (discr L).natAbs =
    HMul.hMul (α := ℕ) ((Ideal.absNorm : (a : Ideal (𝓞 L)) → ℕ) (differentIdeal (𝓞 ↥K₂) (𝓞 L)) : ℕ)
      ((discr.{u_3} ↥K₂).natAbs ^ finrank (↥K₂) L)

Tactic:
have h_main := natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow K₂ (𝓞 K₂) L (𝓞 L)
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
L : Type u_3
inst : Field L
inst_1 : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime.{u_3} (R := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 ↥K₁) (F := 𝓞 ↥K₁ →+* 𝓞 L) (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (R := 𝓞 ↥K₂) (F := 𝓞 ↥K₂ →+* 𝓞 L) (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
h_main :
  (discr L).natAbs =
    HMul.hMul (α := ℕ) ((Ideal.absNorm : (a : Ideal (𝓞 L)) → ℕ) (differentIdeal (𝓞 ↥K₂) (𝓞 L)) : ℕ)
      ((discr.{u_3} ↥K₂).natAbs ^ finrank (↥K₂) L)
rwa rwa₁ rwa₂ rwa₃ : K₁.LinearDisjoint ↥K₂
⊢ K₂.LinearDisjoint ↥K₁

Tactic:
rwa [linearDisjoint_comm]

Premises used: IntermediateField.linearDisjoint_comm
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
L : Type u_3
inst : Field L
inst_1 : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime.{u_3} (R := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 ↥K₁) (F := 𝓞 ↥K₁ →+* 𝓞 L) (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (R := 𝓞 ↥K₂) (F := 𝓞 ↥K₂ →+* 𝓞 L) (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
h_main :
  (discr L).natAbs =
    HMul.hMul (α := ℕ) ((Ideal.absNorm : (a : Ideal (𝓞 L)) → ℕ) (differentIdeal (𝓞 ↥K₂) (𝓞 L)) : ℕ)
      ((discr.{u_3} ↥K₂).natAbs ^ finrank (↥K₂) L)
rwa rwa₁ rwa₂ rwa₃ : K₁ ⊔ K₂ = ⊤
⊢ K₂ ⊔ K₁ = ⊤

Tactic:
rwa [sup_comm]

Premises used: sup_comm
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
L : Type u_3
inst : Field L
inst_1 : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime.{u_3} (R := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 ↥K₁) (F := 𝓞 ↥K₁ →+* 𝓞 L) (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (R := 𝓞 ↥K₂) (F := 𝓞 ↥K₂ →+* 𝓞 L) (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
h_main :
  (discr L).natAbs =
    HMul.hMul (α := ℕ) ((Ideal.absNorm : (a : Ideal (𝓞 L)) → ℕ) (differentIdeal (𝓞 ↥K₂) (𝓞 L)) : ℕ)
      ((discr.{u_3} ↥K₂).natAbs ^ finrank (↥K₂) L)
rwa rwa₁ rwa₂ rwa₃ :
  IsCoprime.{u_3} (R := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 ↥K₁) (F := 𝓞 ↥K₁ →+* 𝓞 L) (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (R := 𝓞 ↥K₂) (F := 𝓞 ↥K₂ →+* 𝓞 L) (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
⊢ IsCoprime.{u_3} (R := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 ↥K₂) (F := 𝓞 ↥K₂ →+* 𝓞 L) (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
    (Ideal.map (R := 𝓞 ↥K₁) (F := 𝓞 ↥K₁ →+* 𝓞 L) (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))

Tactic:
rwa [isCoprime_comm]

Premises used: isCoprime_comm
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
L : Type u_3
inst : Field L
inst_1 : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime.{u_3} (R := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 ↥K₁) (F := 𝓞 ↥K₁ →+* 𝓞 L) (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (R := 𝓞 ↥K₂) (F := 𝓞 ↥K₂ →+* 𝓞 L) (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
h_main :
  (discr L).natAbs =
    HMul.hMul (α := ℕ) ((Ideal.absNorm : (a : Ideal (𝓞 L)) → ℕ) (differentIdeal (𝓞 ↥K₂) (𝓞 L)) : ℕ)
      ((discr.{u_3} ↥K₂).natAbs ^ finrank (↥K₂) L)
rwa :
  ∀
    (h_main :
      (discr L).natAbs =
        (discr.{u_3} ↥K₁).natAbs ^ finrank.{u_3, u_3} (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) *
          (discr.{u_3} ↥K₂).natAbs ^ finrank.{0, u_3} ℚ ↥K₁),
    Eq (α := FractionRing (𝓞 ↥K₁) →+* L)
      (@RingHom.comp _ ↥K₁ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥K₁) L)
        (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (FractionRing.algEquiv (𝓞 ↥K₁) ↥K₁))))
      (RingHom.comp (β := FractionRing (𝓞 L))
        (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (FractionRing.algEquiv (𝓞 L) L)))
        (algebraMap (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L))))
⊢ (discr L).natAbs =
    (discr.{u_3} ↥K₁).natAbs ^ finrank.{0, u_3} ℚ ↥K₂ * (discr.{u_3} ↥K₂).natAbs ^ finrank.{0, u_3} ℚ ↥K₁

Tactic:
rwa [differentIdeal_eq_map_differentIdeal ℤ (𝓞 L) (𝓞 K₂) (𝓞 K₁) (F₁ := K₂) (F₂ := K₁)
    (by rwa [linearDisjoint_comm]) (by rwa [sup_comm]) (by rwa [isCoprime_comm]),
    Ideal.absNorm_algebraMap, absNorm_differentIdeal K₁, h₁.finrank_right_eq_finrank h₂,
    Algebra.finrank_eq_of_equiv_equiv (FractionRing.algEquiv _ K₁).toRingEquiv
    (FractionRing.algEquiv _ L).toRingEquiv, h₁.finrank_left_eq_finrank h₂] at h_main

Premises used: Membership.mem, Subtype, IntermediateField.LinearDisjoint.finrank_right_eq_finrank, IntermediateField.LinearDisjoint.finrank_left_eq_finrank, Int, FractionRing.algEquiv, IsDedekindDomain.differentIdeal_eq_map_differentIdeal, Algebra.finrank_eq_of_equiv_equiv, NumberField.absNorm_differentIdeal, AlgEquiv.toRingEquiv, NumberField.RingOfIntegers, Ideal.absNorm_algebraMap
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
L : Type u_3
inst : Field L
inst_1 : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime.{u_3} (R := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 ↥K₁) (F := 𝓞 ↥K₁ →+* 𝓞 L) (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (R := 𝓞 ↥K₂) (F := 𝓞 ↥K₂ →+* 𝓞 L) (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
h_main :
  (discr L).natAbs =
    (discr.{u_3} ↥K₁).natAbs ^ finrank.{u_3, u_3} (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) *
      (discr.{u_3} ↥K₂).natAbs ^ finrank.{0, u_3} ℚ ↥K₁
a :
  ∀ (x : FractionRing (𝓞 ↥K₁)),
    Eq (α := L)
      ((@RingHom.comp _ ↥K₁ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥K₁) L)
              (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (FractionRing.algEquiv (𝓞 ↥K₁) ↥K₁))) :
            (a : FractionRing (𝓞 ↥K₁)) → L)
          x :
        L)
      ((RingHom.comp (β := FractionRing (𝓞 L))
              (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (FractionRing.algEquiv (𝓞 L) L)))
              (algebraMap (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L))) :
            (a : FractionRing (𝓞 ↥K₁)) → L)
          x :
        L)
⊢ Eq (α := FractionRing (𝓞 ↥K₁) →+* L)
    (@RingHom.comp _ ↥K₁ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥K₁) L)
      (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (FractionRing.algEquiv (𝓞 ↥K₁) ↥K₁))))
    (RingHom.comp (β := FractionRing (𝓞 L)) (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (FractionRing.algEquiv (𝓞 L) L)))
      (algebraMap (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L))))

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
L : Type u_3
inst : Field L
inst_1 : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime.{u_3} (R := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 ↥K₁) (F := 𝓞 ↥K₁ →+* 𝓞 L) (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (R := 𝓞 ↥K₂) (F := 𝓞 ↥K₂ →+* 𝓞 L) (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
h_main :
  (discr L).natAbs =
    (discr.{u_3} ↥K₁).natAbs ^ finrank.{u_3, u_3} (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) *
      (discr.{u_3} ↥K₂).natAbs ^ finrank.{0, u_3} ℚ ↥K₁
x_1 : FractionRing (𝓞 ↥K₁)
⊢ Eq (α := L)
    ((@RingHom.comp _ ↥K₁ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥K₁) L)
            (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (FractionRing.algEquiv (𝓞 ↥K₁) ↥K₁))) :
          (a : FractionRing (𝓞 ↥K₁)) → L)
        x_1 :
      L)
    ((RingHom.comp (β := FractionRing (𝓞 L))
            (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (FractionRing.algEquiv (𝓞 L) L)))
            (algebraMap (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L))) :
          (a : FractionRing (𝓞 ↥K₁)) → L)
        x_1 :
      L)

Tactic:
IsFractionRing.algEquiv_commutes (FractionRing.algEquiv (𝓞 K₁) K₁)
    (FractionRing.algEquiv (𝓞 L) L) _

Premises used: Membership.mem, Subtype, FractionRing.algEquiv, IsFractionRing.algEquiv_commutes, NumberField.RingOfIntegers
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
L : Type u_3
inst : Field L
inst_1 : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime.{u_3} (R := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 ↥K₁) (F := 𝓞 ↥K₁ →+* 𝓞 L) (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (R := 𝓞 ↥K₂) (F := 𝓞 ↥K₂ →+* 𝓞 L) (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
h_main :
  (discr L).natAbs =
    (discr.{u_3} ↥K₁).natAbs ^ finrank.{u_3, u_3} (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) *
      (discr.{u_3} ↥K₂).natAbs ^ finrank.{0, u_3} ℚ ↥K₁
x_1 : FractionRing (𝓞 ↥K₁)
⊢ Eq (α := L)
    ((@RingHom.comp _ ↥K₁ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥K₁) L)
            (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (FractionRing.algEquiv (𝓞 ↥K₁) ↥K₁))) :
          (a : FractionRing (𝓞 ↥K₁)) → L)
        x_1 :
      L)
    ((RingHom.comp (β := FractionRing (𝓞 L))
            (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (FractionRing.algEquiv (𝓞 L) L)))
            (algebraMap (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L))) :
          (a : FractionRing (𝓞 ↥K₁)) → L)
        x_1 :
      L)

Tactic:
exact IsFractionRing.algEquiv_commutes (FractionRing.algEquiv (𝓞 K₁) K₁)
    (FractionRing.algEquiv (𝓞 L) L) _

Premises used: Membership.mem, Subtype, FractionRing.algEquiv, IsFractionRing.algEquiv_commutes, NumberField.RingOfIntegers
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
⊢ IsDomain 𝒪

Tactic:
have := (IsIntegralClosure.algebraMap_injective 𝒪 ℤ K).isDomain
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this : IsDomain 𝒪
⊢ IsDedekindDomain 𝒪

Tactic:
have := IsIntegralClosure.isDedekindDomain ℤ ℚ K 𝒪
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this_1 : IsDomain 𝒪
this : IsDedekindDomain 𝒪
⊢ IsFractionRing 𝒪 K

Tactic:
have := IsIntegralClosure.isFractionRing_of_finite_extension ℤ ℚ K 𝒪