awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : IsFractionRing 𝒪 K
inst_5 : IsDedekindDomain 𝒪
inst_6 : CharZero 𝒪
inst_7 : Module.Finite ℤ 𝒪
this_1 :
  HasQuotient.Quotient ↥(↑1 : Submodule 𝒪 K) (B := Submodule 𝒪 ↥(↑1 : Submodule 𝒪 K))
      (Submodule.comap (Submodule.subtype (↑1 : Submodule 𝒪 K))
        (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K) : Submodule 𝒪 K)) ≃ₗ[𝒪]
    HasQuotient.Quotient ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K) (B :=
      Submodule 𝒪 ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
      (Submodule.comap (Submodule.subtype (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
        (↑1 : Submodule 𝒪 K))
this :
  Nat.card.{u_1}
      (HasQuotient.Quotient ↥(↑1 : Submodule 𝒪 K) (B := Submodule 𝒪 ↥(↑1 : Submodule 𝒪 K))
        (Submodule.comap (Submodule.subtype (↑1 : Submodule 𝒪 K))
          (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K) : Submodule 𝒪 K))) =
    Nat.card.{u_1}
      (HasQuotient.Quotient ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K) (B :=
        Submodule 𝒪 ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
        (Submodule.comap (Submodule.subtype (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
          (↑1 : Submodule 𝒪 K)))
b : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := integralBasis K
b' : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K :=
  LinearMap.BilinForm.dualBasis.{u_1, 0, u_1} (V := K) (K := ℚ) (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
    (Algebra.traceForm ℚ K) ⋯ b
hb :
  Eq (α := Submodule ℤ K)
    (Submodule.span ℤ (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (⇑b : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)))
    (Submodule.restrictScalars.{0, u_2, u_1} ℤ (R := 𝒪) 1)
refine_4 :
  ∀ (i j : Free.ChooseBasisIndex ℤ (𝓞 K)),
    b'.toMatrix (⇑b : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K) i j =
      (RingHom.mapMatrix (algebraMap ℤ ℚ) :
          (a : Matrix (Free.ChooseBasisIndex ℤ (𝓞 K)) (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ) →
            Matrix (Free.ChooseBasisIndex ℤ (𝓞 K)) (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ)
        (Algebra.traceMatrix ℤ (B := 𝓞 K)
          (⇑(RingOfIntegers.basis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (𝓞 K)) :
            (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → 𝓞 K))
        i j
⊢ Eq (α := Matrix (Free.ChooseBasisIndex ℤ (𝓞 K)) (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ)
    (b'.toMatrix (⇑b : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K))
    ((RingHom.mapMatrix (algebraMap ℤ ℚ) :
        (a : Matrix (Free.ChooseBasisIndex ℤ (𝓞 K)) (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ) →
          Matrix (Free.ChooseBasisIndex ℤ (𝓞 K)) (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ)
      (Algebra.traceMatrix ℤ (B := 𝓞 K)
        (⇑(RingOfIntegers.basis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (𝓞 K)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → 𝓞 K)))

Tactic:
ext i j
-- 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 : IsFractionRing 𝒪 K
inst_5 : IsDedekindDomain 𝒪
inst_6 : CharZero 𝒪
inst_7 : Module.Finite ℤ 𝒪
this_1 :
  HasQuotient.Quotient ↥(↑1 : Submodule 𝒪 K) (B := Submodule 𝒪 ↥(↑1 : Submodule 𝒪 K))
      (Submodule.comap (Submodule.subtype (↑1 : Submodule 𝒪 K))
        (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K) : Submodule 𝒪 K)) ≃ₗ[𝒪]
    HasQuotient.Quotient ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K) (B :=
      Submodule 𝒪 ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
      (Submodule.comap (Submodule.subtype (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
        (↑1 : Submodule 𝒪 K))
this :
  Nat.card.{u_1}
      (HasQuotient.Quotient ↥(↑1 : Submodule 𝒪 K) (B := Submodule 𝒪 ↥(↑1 : Submodule 𝒪 K))
        (Submodule.comap (Submodule.subtype (↑1 : Submodule 𝒪 K))
          (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K) : Submodule 𝒪 K))) =
    Nat.card.{u_1}
      (HasQuotient.Quotient ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K) (B :=
        Submodule 𝒪 ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
        (Submodule.comap (Submodule.subtype (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
          (↑1 : Submodule 𝒪 K)))
b : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := integralBasis K
b' : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K :=
  LinearMap.BilinForm.dualBasis.{u_1, 0, u_1} (V := K) (K := ℚ) (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
    (Algebra.traceForm ℚ K) ⋯ b
hb :
  Eq (α := Submodule ℤ K)
    (Submodule.span ℤ (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (⇑b : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)))
    (Submodule.restrictScalars.{0, u_2, u_1} ℤ (R := 𝒪) 1)
i j : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ b'.toMatrix (⇑b : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K) i j =
    (RingHom.mapMatrix (algebraMap ℤ ℚ) :
        (a : Matrix (Free.ChooseBasisIndex ℤ (𝓞 K)) (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ) →
          Matrix (Free.ChooseBasisIndex ℤ (𝓞 K)) (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ)
      (Algebra.traceMatrix ℤ (B := 𝓞 K)
        (⇑(RingOfIntegers.basis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (𝓞 K)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → 𝓞 K))
      i j

Tactic:
simp [b', Module.Basis.toMatrix_apply, mul_comm (RingOfIntegers.basis K i),
      b, integralBasis_apply, ← map_mul, Algebra.trace_localization ℤ ℤ⁰]

Premises used: NumberField.integralBasis_apply, nonZeroDivisors, Int, Module.Basis.toMatrix_apply, map_mul, Algebra.trace_localization, NumberField.RingOfIntegers.basis, mul_comm, DFunLike.coe
-- 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 : IsFractionRing 𝒪 K
inst_5 : IsDedekindDomain 𝒪
inst_6 : CharZero 𝒪
inst_7 : Module.Finite ℤ 𝒪
⊢ Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑((Ideal.absNorm : (a : Ideal 𝒪) → ℕ) (differentIdeal ℤ 𝒪)) : 𝒪)

Tactic:
have := (differentIdeal ℤ 𝒪).absNorm_mem
-- 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 : 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 : ℤ)
inl :
  ∀ (this : Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K).natAbs : 𝒪))
    (h : discr K = (↑(discr K).natAbs : ℤ)), Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
inl₁ :
  ∀ (this : Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(↑(discr K).natAbs : ℤ) : 𝒪))
    (h : discr K = (↑(discr K).natAbs : ℤ)), Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
inl₂ inl₃ inl₄ inl₅ :
  ∀ (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) : 𝒪)

Tactic:
rwa [absNorm_differentIdeal K, ← Int.cast_natCast, ← h] at this

Premises used: Int.cast_natCast, NumberField.absNorm_differentIdeal
-- 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 : 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) : 𝒪)
inr₄ inr₅ inr₆ 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) : 𝒪)

Tactic:
rwa [absNorm_differentIdeal K, ← Int.cast_natCast, Int.eq_neg_comm.mp h,
      Int.cast_neg, neg_mem_iff] at this

Premises used: Int.cast_neg, Int.cast_natCast, neg_mem_iff, Int.eq_neg_comm, NumberField.absNorm_differentIdeal, Iff.mp
-- 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 : IsFractionRing 𝒪 K
inst_5 : IsDedekindDomain 𝒪
inst_6 : CharZero 𝒪
inst_7 : Module.Finite ℤ 𝒪
this :
  Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑((Ideal.absNorm : (a : Ideal 𝒪) → ℕ) (differentIdeal ℤ 𝒪)) : 𝒪)
⊢ 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

Premises used: Int.cast_neg, Int.cast_natCast, neg_mem_iff, NumberField.absNorm_differentIdeal, Int.natAbs_eq, NumberField.discr
-- 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 : 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 𝒪 𝒪'
⊢ 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 ℤ 𝒪 𝒪')
-- 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 : 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 ℤ 𝒪))) :
      ℕ)
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 𝒪')))
⊢ (discr L).natAbs =
    HMul.hMul (α := ℕ) ((Ideal.absNorm : (a : Ideal 𝒪') → ℕ) (differentIdeal 𝒪 𝒪') : ℕ) ((discr K).natAbs ^ finrank K L)

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

Premises used: FractionRing.algEquiv, Algebra.finrank_eq_of_equiv_equiv, map_mul, NumberField.absNorm_differentIdeal, AlgEquiv.toRingEquiv, Ideal.absNorm_algebraMap
-- 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 : 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 𝒪'))
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)
⊢ 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:
ext
-- 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 : 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 𝒪'))
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:
IsFractionRing.algEquiv_commutes (FractionRing.algEquiv 𝒪 K)
    (FractionRing.algEquiv 𝒪' L) _

Premises used: FractionRing.algEquiv, IsFractionRing.algEquiv_commutes
-- 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 : 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 𝒪'))
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:
exact IsFractionRing.algEquiv_commutes (FractionRing.algEquiv 𝒪 K)
    (FractionRing.algEquiv 𝒪' L) _

Premises used: FractionRing.algEquiv, IsFractionRing.algEquiv_commutes
-- 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
h : IsCoprime (discr K₁) (discr K₂)
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₂)))
⊢ 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
-- 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
⊢ 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:
Ideal.isCoprime_iff_exists.mpr ⟨u * discr K₁, ?_, v * discr K₂, ?_, ?_⟩

Premises used: Iff.mpr, Int.cast, HMul.hMul, Ideal.isCoprime_iff_exists, And.intro, Exists.intro, NumberField.discr
-- 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_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))
refine_3 : HMul.hMul (α := 𝓞 L) (↑u : 𝓞 L) (↑(discr K₁) : 𝓞 L) + HMul.hMul (α := 𝓞 L) (↑v : 𝓞 L) (↑(discr K₂) : 𝓞 L) = 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:
refine Ideal.isCoprime_iff_exists.mpr ⟨u * discr K₁, ?_, v * discr K₂, ?_, ?_⟩

Premises used: Iff.mpr, HMul.hMul, Ideal.isCoprime_iff_exists, And.intro, Exists.intro, NumberField.discr
-- 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_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)
⊢ 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:
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_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₁))
⊢ 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:
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_4, 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