awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsFractionRing 𝒪 K
inst_5 : IsDedekindDomain 𝒪
inst_6 : CharZero 𝒪
inst_7 : Module.Finite ℤ 𝒪
this :
  Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑((Ideal.absNorm : (a : Ideal 𝒪) → ℕ) (differentIdeal ℤ 𝒪)) : 𝒪)
h : discr K = -(↑(discr K).natAbs : ℤ)
inr :
  ∀ (this : Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K).natAbs : 𝒪))
    (h : discr K = -(↑(discr K).natAbs : ℤ)), Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
inr₁ :
  ∀ (this : Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(↑(discr K).natAbs : ℤ) : 𝒪))
    (h : discr K = -(↑(discr K).natAbs : ℤ)), Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
inr₂ :
  ∀ (this : Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(-discr K) : 𝒪))
    (h : discr K = -(↑(discr K).natAbs : ℤ)), Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
inr₃ :
  ∀ (this : Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (-(↑(discr K) : 𝒪)))
    (h : discr K = -(↑(discr K).natAbs : ℤ)), Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
⊢ Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
have inr₄ : ∀ (this : Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)) (h : discr K = -(↑(discr K).natAbs : ℤ)),
  Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
Tactic: rwa [absNorm_differentIdeal K, ← Int.cast_natCast, Int.eq_neg_comm.mp h,
      Int.cast_neg, neg_mem_iff] at this
Cleared hypotheses: this, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (hypothesis)
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsFractionRing 𝒪 K
inst_5 : IsDedekindDomain 𝒪
inst_6 : CharZero 𝒪
inst_7 : Module.Finite ℤ 𝒪
this :
  Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑((Ideal.absNorm : (a : Ideal 𝒪) → ℕ) (differentIdeal ℤ 𝒪)) : 𝒪)
⊢ Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
have x : discr K = (↑(discr K).natAbs : ℤ) ∨ discr K = -(↑(discr K).natAbs : ℤ)
Tactic: cases (discr K).natAbs_eq with
  | inl h =>
    rwa [absNorm_differentIdeal K, ← Int.cast_natCast, ← h] at this
  | inr h =>
    rwa [absNorm_differentIdeal K, ← Int.cast_natCast, Int.eq_neg_comm.mp h,
      Int.cast_neg, neg_mem_iff] at this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (hypothesis)
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsFractionRing 𝒪 K
inst_5 : IsDedekindDomain 𝒪
inst_6 : CharZero 𝒪
inst_7 : Module.Finite ℤ 𝒪
L : Type u_3
𝒪' : Type u_4
inst_8 : Field L
inst_9 : NumberField L
inst_10 : CommRing 𝒪'
inst_11 : Algebra 𝒪' L
inst_12 : IsFractionRing 𝒪' L
inst_13 : IsIntegralClosure 𝒪' ℤ L
inst_14 : IsDedekindDomain 𝒪'
inst_15 : CharZero 𝒪'
inst_16 : Algebra K L
inst_17 : Algebra 𝒪 𝒪'
inst_18 : Algebra 𝒪 L
inst_19 : IsScalarTower 𝒪 K L
inst_20 : IsScalarTower 𝒪 𝒪' L
inst_21 : IsTorsionFree 𝒪 𝒪'
inst_22 : Free ℤ 𝒪'
inst_23 : Module.Finite ℤ 𝒪'
inst_24 : Module.Finite 𝒪 𝒪'
⊢ (discr L).natAbs =
    HMul.hMul (α := ℕ) ((Ideal.absNorm : (a : Ideal 𝒪') → ℕ) (differentIdeal 𝒪 𝒪') : ℕ) ((discr K).natAbs ^ finrank K L)
have this : Eq (α := ℕ) ((Ideal.absNorm : (a : Ideal 𝒪') → ℕ) (differentIdeal ℤ 𝒪') : ℕ)
  ((Ideal.absNorm : (a : Ideal 𝒪') → ℕ)
      (HMul.hMul (α := Ideal 𝒪') (differentIdeal 𝒪 𝒪')
        (Ideal.map (F := 𝒪 →+* 𝒪') (algebraMap 𝒪 𝒪') (differentIdeal ℤ 𝒪))) :
    ℕ)
Tactic: have := congr_arg Ideal.absNorm
    (differentIdeal_eq_differentIdeal_mul_differentIdeal ℤ 𝒪 𝒪')
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsFractionRing 𝒪 K
inst_5 : IsDedekindDomain 𝒪
inst_6 : CharZero 𝒪
inst_7 : Module.Finite ℤ 𝒪
L : Type u_3
𝒪' : Type u_4
inst_8 : Field L
inst_9 : NumberField L
inst_10 : CommRing 𝒪'
inst_11 : Algebra 𝒪' L
inst_12 : IsFractionRing 𝒪' L
inst_13 : IsIntegralClosure 𝒪' ℤ L
inst_14 : IsDedekindDomain 𝒪'
inst_15 : CharZero 𝒪'
inst_16 : Algebra K L
inst_17 : Algebra 𝒪 𝒪'
inst_18 : Algebra 𝒪 L
inst_19 : IsScalarTower 𝒪 K L
inst_20 : IsScalarTower 𝒪 𝒪' L
inst_21 : IsTorsionFree 𝒪 𝒪'
inst_22 : Free ℤ 𝒪'
inst_23 : Module.Finite ℤ 𝒪'
inst_24 : Module.Finite 𝒪 𝒪'
this :
  Eq (α := ℕ) ((Ideal.absNorm : (a : Ideal 𝒪') → ℕ) (differentIdeal ℤ 𝒪') : ℕ)
    ((Ideal.absNorm : (a : Ideal 𝒪') → ℕ)
        (HMul.hMul (α := Ideal 𝒪') (differentIdeal 𝒪 𝒪')
          (Ideal.map (F := 𝒪 →+* 𝒪') (algebraMap 𝒪 𝒪') (differentIdeal ℤ 𝒪))) :
      ℕ)
⊢ (discr L).natAbs =
    HMul.hMul (α := ℕ) ((Ideal.absNorm : (a : Ideal 𝒪') → ℕ) (differentIdeal 𝒪 𝒪') : ℕ) ((discr K).natAbs ^ finrank K L)
have rwa : ∀
  (this :
    (discr L).natAbs =
      HMul.hMul (α := ℕ) ((Ideal.absNorm : (a : Ideal 𝒪') → ℕ) (differentIdeal 𝒪 𝒪') : ℕ)
        ((discr K).natAbs ^ finrank.{u_2, u_4} (FractionRing 𝒪) (FractionRing 𝒪'))),
  Eq (α := RingHom.{u_2, u_3} (FractionRing 𝒪) L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L)
      (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (FractionRing.algEquiv 𝒪 K))))
    (RingHom.comp (β := FractionRing 𝒪') (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (FractionRing.algEquiv 𝒪' L)))
      (algebraMap (FractionRing 𝒪) (FractionRing 𝒪')))
Tactic: rwa [absNorm_differentIdeal L, map_mul, Ideal.absNorm_algebraMap,
    absNorm_differentIdeal K, Algebra.finrank_eq_of_equiv_equiv
      (FractionRing.algEquiv 𝒪 K).toRingEquiv (FractionRing.algEquiv 𝒪' L).toRingEquiv] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsFractionRing 𝒪 K
inst_5 : IsDedekindDomain 𝒪
inst_6 : CharZero 𝒪
inst_7 : Module.Finite ℤ 𝒪
L : Type u_3
𝒪' : Type u_4
inst_8 : Field L
inst_9 : NumberField L
inst_10 : CommRing 𝒪'
inst_11 : Algebra 𝒪' L
inst_12 : IsFractionRing 𝒪' L
inst_13 : IsIntegralClosure 𝒪' ℤ L
inst_14 : IsDedekindDomain 𝒪'
inst_15 : CharZero 𝒪'
inst_16 : Algebra K L
inst_17 : Algebra 𝒪 𝒪'
inst_18 : Algebra 𝒪 L
inst_19 : IsScalarTower 𝒪 K L
inst_20 : IsScalarTower 𝒪 𝒪' L
inst_21 : IsTorsionFree 𝒪 𝒪'
inst_22 : Free ℤ 𝒪'
inst_23 : Module.Finite ℤ 𝒪'
inst_24 : Module.Finite 𝒪 𝒪'
this :
  (discr L).natAbs =
    HMul.hMul (α := ℕ) ((Ideal.absNorm : (a : Ideal 𝒪') → ℕ) (differentIdeal 𝒪 𝒪') : ℕ)
      ((discr K).natAbs ^ finrank.{u_2, u_4} (FractionRing 𝒪) (FractionRing 𝒪'))
⊢ Eq (α := RingHom.{u_2, u_3} (FractionRing 𝒪) L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L)
      (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (FractionRing.algEquiv 𝒪 K))))
    (RingHom.comp (β := FractionRing 𝒪') (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (FractionRing.algEquiv 𝒪' L)))
      (algebraMap (FractionRing 𝒪) (FractionRing 𝒪')))
have a : ∀ (x : FractionRing 𝒪),
  Eq.{u_3 + 1} (α := L)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L)
            (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (FractionRing.algEquiv 𝒪 K))) :
          (a : FractionRing 𝒪) → L)
        x :
      L)
    ((RingHom.comp (β := FractionRing 𝒪') (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (FractionRing.algEquiv 𝒪' L)))
            (algebraMap (FractionRing 𝒪) (FractionRing 𝒪')) :
          (a : FractionRing 𝒪) → L)
        x :
      L)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
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
h : IsCoprime (discr K₁) (discr K₂)
⊢ IsCoprime.{u_3} (R := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 K₁) (F := RingHom.{u_4, u_3} (𝓞 K₁) (𝓞 L)) (algebraMap (𝓞 K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 K₁)))
    (Ideal.map (R := 𝓞 K₂) (F := RingHom.{u_5, u_3} (𝓞 K₂) (𝓞 L)) (algebraMap (𝓞 K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 K₂)))
have obtain : ∀ (u v : ℤ) (h : u * discr K₁ + v * discr K₂ = 1),
  IsCoprime.{u_3} (R := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 K₁) (F := RingHom.{u_4, u_3} (𝓞 K₁) (𝓞 L)) (algebraMap (𝓞 K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 K₁)))
    (Ideal.map (R := 𝓞 K₂) (F := RingHom.{u_5, u_3} (𝓞 K₂) (𝓞 L)) (algebraMap (𝓞 K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 K₂)))
Tactic: obtain ⟨u, v, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
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
⊢ IsCoprime.{u_3} (R := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 K₁) (F := RingHom.{u_4, u_3} (𝓞 K₁) (𝓞 L)) (algebraMap (𝓞 K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 K₁)))
    (Ideal.map (R := 𝓞 K₂) (F := RingHom.{u_5, u_3} (𝓞 K₂) (𝓞 L)) (algebraMap (𝓞 K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 K₂)))
have refine_1 : Membership.mem (γ := Ideal (𝓞 L))
  (Ideal.map (R := 𝓞 K₁) (F := RingHom.{u_4, u_3} (𝓞 K₁) (𝓞 L)) (algebraMap (𝓞 K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 K₁)))
  (HMul.hMul (α := 𝓞 L) (↑u : 𝓞 L) (↑(discr K₁) : 𝓞 L))
Tactic: refine Ideal.isCoprime_iff_exists.mpr ⟨u * discr K₁, ?_, v * discr K₂, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
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_1 :
  Membership.mem (γ := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 K₁) (F := RingHom.{u_4, u_3} (𝓞 K₁) (𝓞 L)) (algebraMap (𝓞 K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 K₁)))
    (HMul.hMul (α := 𝓞 L) (↑u : 𝓞 L) (↑(discr K₁) : 𝓞 L))
⊢ IsCoprime.{u_3} (R := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 K₁) (F := RingHom.{u_4, u_3} (𝓞 K₁) (𝓞 L)) (algebraMap (𝓞 K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 K₁)))
    (Ideal.map (R := 𝓞 K₂) (F := RingHom.{u_5, u_3} (𝓞 K₂) (𝓞 L)) (algebraMap (𝓞 K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 K₂)))
have refine_2 : 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: refine Ideal.isCoprime_iff_exists.mpr ⟨u * discr K₁, ?_, v * discr K₂, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
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_1 :
  Membership.mem (γ := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 K₁) (F := RingHom.{u_4, u_3} (𝓞 K₁) (𝓞 L)) (algebraMap (𝓞 K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 K₁)))
    (HMul.hMul (α := 𝓞 L) (↑u : 𝓞 L) (↑(discr K₁) : 𝓞 L))
refine_2 :
  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))
⊢ IsCoprime.{u_3} (R := Ideal (𝓞 L))
    (Ideal.map (R := 𝓞 K₁) (F := RingHom.{u_4, u_3} (𝓞 K₁) (𝓞 L)) (algebraMap (𝓞 K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 K₁)))
    (Ideal.map (R := 𝓞 K₂) (F := RingHom.{u_5, u_3} (𝓞 K₂) (𝓞 L)) (algebraMap (𝓞 K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 K₂)))
have refine_3 : HMul.hMul (α := 𝓞 L) (↑u : 𝓞 L) (↑(discr K₁) : 𝓞 L) + HMul.hMul (α := 𝓞 L) (↑v : 𝓞 L) (↑(discr K₂) : 𝓞 L) = 1
Tactic: refine Ideal.isCoprime_iff_exists.mpr ⟨u * discr K₁, ?_, v * discr K₂, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
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₁)))
    (HMul.hMul (α := 𝓞 L) (↑u : 𝓞 L) (↑(discr K₁) : 𝓞 L))
have refine_1 : Membership.mem (γ := Ideal (𝓞 L))
  (Ideal.map (R := 𝓞 K₁) (F := RingHom.{u_4, u_3} (𝓞 K₁) (𝓞 L)) (algebraMap (𝓞 K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 K₁)))
  (↑(discr K₁) : 𝓞 L)
Tactic: apply Ideal.mul_mem_left
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
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₁)))
    (↑(discr K₁) : 𝓞 L)
have refine_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: rw [← map_intCast (algebraMap (𝓞 K₁) (𝓞 L))]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
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₂)))
    (HMul.hMul (α := 𝓞 L) (↑v : 𝓞 L) (↑(discr K₂) : 𝓞 L))
have 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)
Tactic: apply Ideal.mul_mem_left
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
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₂)))
    (↑(discr K₂) : 𝓞 L)
have 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₂))
Tactic: rw [← map_intCast (algebraMap (𝓞 K₂) (𝓞 L))]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
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
⊢ HMul.hMul (α := 𝓞 L) (↑u : 𝓞 L) (↑(discr K₁) : 𝓞 L) + HMul.hMul (α := 𝓞 L) (↑v : 𝓞 L) (↑(discr K₂) : 𝓞 L) = 1
have refine_3 : (↑(u * 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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
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
⊢ HMul.hMul (α := 𝓞 L) (↑u : 𝓞 L) (↑(discr K₁) : 𝓞 L) + HMul.hMul (α := 𝓞 L) (↑v : 𝓞 L) (↑(discr K₂) : 𝓞 L) = 1
have refine_3₁ : HAdd.hAdd (α := 𝓞 L) (↑(u * discr K₁) : 𝓞 L) (↑(v * discr K₂) : 𝓞 L) = 1
Tactic: rw [← Int.cast_mul, ← Int.cast_mul, ← Int.cast_add, h, Int.cast_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
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
⊢ HMul.hMul (α := 𝓞 L) (↑u : 𝓞 L) (↑(discr K₁) : 𝓞 L) + HMul.hMul (α := 𝓞 L) (↑v : 𝓞 L) (↑(discr K₂) : 𝓞 L) = 1
have refine_3₂ : Eq.{u_3 + 1} (α := 𝓞 L) (↑(u * discr K₁ + v * discr K₂) : 𝓞 L) 1
Tactic: rw [← Int.cast_mul, ← Int.cast_mul, ← Int.cast_add, h, Int.cast_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
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
⊢ HMul.hMul (α := 𝓞 L) (↑u : 𝓞 L) (↑(discr K₁) : 𝓞 L) + HMul.hMul (α := 𝓞 L) (↑v : 𝓞 L) (↑(discr K₂) : 𝓞 L) = 1
have refine_3₃ : Eq.{u_3 + 1} (α := 𝓞 L) (↑1 : 𝓞 L) 1
Tactic: rw [← Int.cast_mul, ← Int.cast_mul, ← Int.cast_add, h, Int.cast_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
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
⊢ HMul.hMul (α := 𝓞 L) (↑u : 𝓞 L) (↑(discr K₁) : 𝓞 L) + HMul.hMul (α := 𝓞 L) (↑v : 𝓞 L) (↑(discr K₂) : 𝓞 L) = 1
have refine_3₄ : Eq.{u_3 + 1} (α := 𝓞 L) 1 1
Tactic: rw [← Int.cast_mul, ← Int.cast_mul, ← Int.cast_add, h, Int.cast_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
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 ∣ discr L
have suffices : discr K ^ finrank K L ∣ 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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
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 L
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
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₂)
⊢ K₁.LinearDisjoint ↥K₂
have h₁ : K₁ ⊓ K₂ = ⊥
Tactic: apply IntermediateField.LinearDisjoint.of_inf_eq_bot
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
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₂))
⊢ K₁ ⊓ K₂ = ⊥
have contrapose! : ∀ (this : K₁ ⊓ K₂ ≠ ⊥), ¬IsUnit (discr.{u_3} ↥(K₁ ⊓ K₂))
Tactic: contrapose! this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
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₂)
have refine : finrank.{0, u_3} ℚ ↥(K₁ ⊓ K₂) ≠ 1
Tactic: refine Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨Module.finrank_pos.ne', ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
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₂ ≠ ⊥
⊢ finrank.{0, u_3} ℚ ↥(K₁ ⊓ K₂) ≠ 1
have rwa : ∀ (this : ¬K₁ ⊓ K₂ = ⊥), finrank.{0, u_3} ℚ ↥(K₁ ⊓ K₂) ≠ 1
Tactic: rwa [ne_eq, ← IntermediateField.finrank_eq_one_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
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
⊢ finrank.{0, u_3} ℚ ↥(K₁ ⊓ K₂) ≠ 1
have rwa₁ : ∀ (this : ¬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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (hypothesis)
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₂ ≠ ⊥
⊢ ¬IsUnit (discr.{u_3} ↥(K₁ ⊓ K₂))
have this₁ : 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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
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₂)
⊢ ¬|discr.{u_3} ↥(K₁ ⊓ K₂)| = 1
have 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
Tactic: linarith [abs_discr_gt_two this]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
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
⊢ ¬|discr.{u_3} ↥(K₁ ⊓ K₂)| = 1
have linarith₁ : |discr.{u_3} ↥(K₁ ⊓ K₂)| = 1 → GT.gt (α := ℤ) 2 0
Tactic: linarith [abs_discr_gt_two this]