awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.LinearDisjoint (goal)
Goal:
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : CommRing B
inst_5 : Field L
inst_6 : Algebra B L
inst_7 : Algebra A L
inst_8 : Algebra K L
inst_9 : FiniteDimensional K L
inst_10 : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst_11 : CommRing R₁
inst_12 : CommRing R₂
inst_13 : IsDomain R₁
inst_14 : Algebra A R₁
inst_15 : Algebra A R₂
inst_16 : Algebra R₁ B
inst_17 : Algebra R₂ B
inst_18 : Algebra R₁ L
inst_19 : Algebra R₂ L
inst_20 : IsScalarTower A R₁ L
inst_21 : IsScalarTower R₁ B L
inst_22 : IsScalarTower R₂ B L
inst_23 : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst_24 : Algebra.{u_5, u_4} R₁ ↥F₁
inst_25 : Algebra.{u_6, u_4} R₂ ↥F₂
inst_26 : IsTorsionFree.{u_5, u_4} R₁ ↥F₁
inst_27 : IsScalarTower A (↥F₂) L
inst_28 : IsScalarTower.{u_1, u_6, u_4} A R₂ ↥F₂
inst_29 : IsScalarTower R₁ (↥F₁) L
inst_30 : IsScalarTower R₂ (↥F₂) L
inst_31 : Algebra.IsSeparable.{u_3, u_4} K ↥F₂
inst_32 : Algebra.IsSeparable (↥F₁) L
inst_33 : IsDomain A
inst_34 : IsDedekindDomain B
inst_35 : IsDedekindDomain R₁
inst_36 : IsDedekindDomain R₂
inst_37 : IsFractionRing B L
inst_38 : IsFractionRing.{u_5, u_4} R₁ ↥F₁
inst_39 : IsFractionRing.{u_6, u_4} R₂ ↥F₂
inst_40 : IsIntegrallyClosed A
inst_41 : IsIntegralClosure B R₁ L
inst_42 : IsTorsionFree R₁ B
inst_43 : IsTorsionFree R₂ B
inst_44 : Algebra A B
inst_45 : Module.Finite A B
inst_46 : IsTorsionFree A B
inst_47 : IsTorsionFree A R₁
inst_48 : IsTorsionFree A R₂
inst_49 : Module.Finite A R₁
inst_50 : Module.Finite R₂ B
inst_51 : IsScalarTower A R₂ B
inst_52 : Module.Finite R₁ B
inst_53 : Algebra.IsSeparable.{u_1, u_2} (FractionRing A) (FractionRing B)
inst_54 : IsScalarTower A R₁ B
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
h₃ :
  IsCoprime.{u_2} (R := Ideal B) (Ideal.map (F := R₁ →+* B) (algebraMap R₁ B) (differentIdeal A R₁))
    (Ideal.map (F := R₂ →+* B) (algebraMap R₂ B) (differentIdeal A R₂))
ι : Type u_7
b : Basis ι A R₂
this : Free A R₂
v : (i : ι) → B := fun (i : ι) ↦ (algebraMap R₂ B : (a : R₂) → B) ((b : (a : ι) → R₂) i : R₂)
b₂ : Basis.{u_7, u_3, u_4} ι K ↥F₂ := localizationLocalization.{u_1, u_3, u_6, u_4, u_7} (R := A) K A⁰ (A := R₂) (↥F₂) b
P₁ : LinearIndependent R₁ v
h :
  Eq (α := ι → L) ((⇑(AlgHom.toLinearMap (IsScalarTower.toAlgHom R₁ B L)) : (a : B) → L) ∘ v)
    (⇑(h₁.basisOfBasisRight h₂ b₂) : (a : ι) → L)
⊢ Eq (α := Submodule R₁ L)
    (span R₁ (Set.range ((⇑(AlgHom.toLinearMap (IsScalarTower.toAlgHom R₁ B L)) : (a : B) → L) ∘ v)))
    (Submodule.map (AlgHom.toLinearMap (IsScalarTower.toAlgHom R₁ B L)) ⊤)
have h₄ : Eq (α := Submodule R₁ L) (Submodule.map (AlgHom.toLinearMap (IsScalarTower.toAlgHom R₁ B L)) ⊤)
  (Submodule.restrictScalars.{u_5, u_2, u_4} R₁ (R := B) 1)
Tactic: convert!
      Module.Basis.ofIsCoprimeDifferentIdeal_aux A B R₁ R₂ h₁ h₂ h₃ b₂
        (b.localizationLocalization_span K A⁰ F₂)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.LinearDisjoint (goal)
Goal:
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : CommRing B
inst_5 : Field L
inst_6 : Algebra B L
inst_7 : Algebra A L
inst_8 : Algebra K L
inst_9 : FiniteDimensional K L
inst_10 : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst_11 : CommRing R₁
inst_12 : CommRing R₂
inst_13 : IsDomain R₁
inst_14 : Algebra A R₁
inst_15 : Algebra A R₂
inst_16 : Algebra R₁ B
inst_17 : Algebra R₂ B
inst_18 : Algebra R₁ L
inst_19 : Algebra R₂ L
inst_20 : IsScalarTower A R₁ L
inst_21 : IsScalarTower R₁ B L
inst_22 : IsScalarTower R₂ B L
inst_23 : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst_24 : Algebra.{u_5, u_4} R₁ ↥F₁
inst_25 : Algebra.{u_6, u_4} R₂ ↥F₂
inst_26 : IsTorsionFree.{u_5, u_4} R₁ ↥F₁
inst_27 : IsScalarTower A (↥F₂) L
inst_28 : IsScalarTower.{u_1, u_6, u_4} A R₂ ↥F₂
inst_29 : IsScalarTower R₁ (↥F₁) L
inst_30 : IsScalarTower R₂ (↥F₂) L
inst_31 : Algebra.IsSeparable.{u_3, u_4} K ↥F₂
inst_32 : Algebra.IsSeparable (↥F₁) L
inst_33 : IsDomain A
inst_34 : IsDedekindDomain B
inst_35 : IsDedekindDomain R₁
inst_36 : IsDedekindDomain R₂
inst_37 : IsFractionRing B L
inst_38 : IsFractionRing.{u_5, u_4} R₁ ↥F₁
inst_39 : IsFractionRing.{u_6, u_4} R₂ ↥F₂
inst_40 : IsIntegrallyClosed A
inst_41 : IsIntegralClosure B R₁ L
inst_42 : IsTorsionFree R₁ B
inst_43 : IsTorsionFree R₂ B
inst_44 : Algebra A B
inst_45 : Module.Finite A B
inst_46 : IsTorsionFree A B
inst_47 : IsTorsionFree A R₁
inst_48 : IsTorsionFree A R₂
inst_49 : Module.Finite A R₁
inst_50 : Module.Finite R₂ B
inst_51 : IsScalarTower A R₂ B
inst_52 : Module.Finite R₁ B
inst_53 : Algebra.IsSeparable.{u_1, u_2} (FractionRing A) (FractionRing B)
inst_54 : IsScalarTower A R₁ B
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
h₃ :
  IsCoprime.{u_2} (R := Ideal B) (Ideal.map (F := R₁ →+* B) (algebraMap R₁ B) (differentIdeal A R₁))
    (Ideal.map (F := R₂ →+* B) (algebraMap R₂ B) (differentIdeal A R₂))
ι : Type u_7
b : Basis ι A R₂
this : Free A R₂
v : (i : ι) → B := fun (i : ι) ↦ (algebraMap R₂ B : (a : R₂) → B) ((b : (a : ι) → R₂) i : R₂)
b₂ : Basis.{u_7, u_3, u_4} ι K ↥F₂ := localizationLocalization.{u_1, u_3, u_6, u_4, u_7} (R := A) K A⁰ (A := R₂) (↥F₂) b
P₁ : LinearIndependent R₁ v
⊢ Eq (α := ι → L) ((⇑(AlgHom.toLinearMap (IsScalarTower.toAlgHom R₁ B L)) : (a : B) → L) ∘ v)
    (⇑(h₁.basisOfBasisRight h₂ b₂) : (a : ι) → L)
have h : ∀ (x : ι),
  Eq.{u_4 + 1} (α := L) (((⇑(AlgHom.toLinearMap (IsScalarTower.toAlgHom R₁ B L)) : (a : B) → L) ∘ v) x : L)
    ((h₁.basisOfBasisRight h₂ b₂ : (a : ι) → L) x : L)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.LinearDisjoint (goal)
Goal:
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : CommRing B
inst_5 : Field L
inst_6 : Algebra B L
inst_7 : Algebra A L
inst_8 : Algebra K L
inst_9 : FiniteDimensional K L
inst_10 : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst_11 : CommRing R₁
inst_12 : CommRing R₂
inst_13 : IsDomain R₁
inst_14 : Algebra A R₁
inst_15 : Algebra A R₂
inst_16 : Algebra R₁ B
inst_17 : Algebra R₂ B
inst_18 : Algebra R₁ L
inst_19 : Algebra R₂ L
inst_20 : IsScalarTower A R₁ L
inst_21 : IsScalarTower R₁ B L
inst_22 : IsScalarTower R₂ B L
inst_23 : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst_24 : Algebra.{u_5, u_4} R₁ ↥F₁
inst_25 : Algebra.{u_6, u_4} R₂ ↥F₂
inst_26 : IsTorsionFree.{u_5, u_4} R₁ ↥F₁
inst_27 : IsScalarTower A (↥F₂) L
inst_28 : IsScalarTower.{u_1, u_6, u_4} A R₂ ↥F₂
inst_29 : IsScalarTower R₁ (↥F₁) L
inst_30 : IsScalarTower R₂ (↥F₂) L
inst_31 : Algebra.IsSeparable.{u_3, u_4} K ↥F₂
inst_32 : Algebra.IsSeparable (↥F₁) L
inst_33 : IsDomain A
inst_34 : IsDedekindDomain B
inst_35 : IsDedekindDomain R₁
inst_36 : IsDedekindDomain R₂
inst_37 : IsFractionRing B L
inst_38 : IsFractionRing.{u_5, u_4} R₁ ↥F₁
inst_39 : IsFractionRing.{u_6, u_4} R₂ ↥F₂
inst_40 : IsIntegrallyClosed A
inst_41 : IsIntegralClosure B R₁ L
inst_42 : IsTorsionFree R₁ B
inst_43 : IsTorsionFree R₂ B
inst_44 : Algebra A B
inst_45 : Module.Finite A B
inst_46 : IsTorsionFree A B
inst_47 : IsTorsionFree A R₁
inst_48 : IsTorsionFree A R₂
inst_49 : Module.Finite A R₁
inst_50 : Module.Finite R₂ B
inst_51 : IsScalarTower A R₂ B
inst_52 : Module.Finite R₁ B
inst_53 : Algebra.IsSeparable.{u_1, u_2} (FractionRing A) (FractionRing B)
inst_54 : IsScalarTower A R₁ B
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
h₃ :
  IsCoprime.{u_2} (R := Ideal B) (Ideal.map (F := R₁ →+* B) (algebraMap R₁ B) (differentIdeal A R₁))
    (Ideal.map (F := R₂ →+* B) (algebraMap R₂ B) (differentIdeal A R₂))
ι : Type u_7
b : Basis ι A R₂
this : Free A R₂
v : (i : ι) → B := fun (i : ι) ↦ (algebraMap R₂ B : (a : R₂) → B) ((b : (a : ι) → R₂) i : R₂)
b₂ : Basis.{u_7, u_3, u_4} ι K ↥F₂ := localizationLocalization.{u_1, u_3, u_6, u_4, u_7} (R := A) K A⁰ (A := R₂) (↥F₂) b
P₁ : LinearIndependent R₁ v
⊢ Eq (α := Submodule R₁ L) (Submodule.map (AlgHom.toLinearMap (IsScalarTower.toAlgHom R₁ B L)) ⊤)
    (Submodule.restrictScalars.{u_5, u_2, u_4} R₁ (R := B) 1)
have h : ∀ (x : L),
  Membership.mem (γ := Submodule R₁ L) (Submodule.map (AlgHom.toLinearMap (IsScalarTower.toAlgHom R₁ B L)) ⊤) x ↔
    Membership.mem (γ := Submodule R₁ L) (Submodule.restrictScalars.{u_5, u_2, u_4} R₁ (R := B) 1) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.LinearDisjoint (goal)
Goal:
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : CommRing B
inst_5 : Field L
inst_6 : Algebra B L
inst_7 : Algebra A L
inst_8 : Algebra K L
inst_9 : FiniteDimensional K L
inst_10 : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst_11 : CommRing R₁
inst_12 : CommRing R₂
inst_13 : IsDomain R₁
inst_14 : Algebra A R₁
inst_15 : Algebra A R₂
inst_16 : Algebra R₁ B
inst_17 : Algebra R₂ B
inst_18 : Algebra R₁ L
inst_19 : Algebra R₂ L
inst_20 : IsScalarTower A R₁ L
inst_21 : IsScalarTower R₁ B L
inst_22 : IsScalarTower R₂ B L
inst_23 : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst_24 : Algebra.{u_5, u_4} R₁ ↥F₁
inst_25 : Algebra.{u_6, u_4} R₂ ↥F₂
inst_26 : IsTorsionFree.{u_5, u_4} R₁ ↥F₁
inst_27 : IsScalarTower A (↥F₂) L
inst_28 : IsScalarTower.{u_1, u_6, u_4} A R₂ ↥F₂
inst_29 : IsScalarTower R₁ (↥F₁) L
inst_30 : IsScalarTower R₂ (↥F₂) L
inst_31 : Algebra.IsSeparable.{u_3, u_4} K ↥F₂
inst_32 : Algebra.IsSeparable (↥F₁) L
inst_33 : IsDomain A
inst_34 : IsDedekindDomain B
inst_35 : IsDedekindDomain R₁
inst_36 : IsDedekindDomain R₂
inst_37 : IsFractionRing B L
inst_38 : IsFractionRing.{u_5, u_4} R₁ ↥F₁
inst_39 : IsFractionRing.{u_6, u_4} R₂ ↥F₂
inst_40 : IsIntegrallyClosed A
inst_41 : IsIntegralClosure B R₁ L
inst_42 : IsTorsionFree R₁ B
inst_43 : IsTorsionFree R₂ B
inst_44 : Algebra A B
inst_45 : Module.Finite A B
inst_46 : IsTorsionFree A B
inst_47 : IsTorsionFree A R₁
inst_48 : IsTorsionFree A R₂
inst_49 : Module.Finite A R₁
inst_50 : Module.Finite R₂ B
inst_51 : IsScalarTower A R₂ B
inst_52 : Module.Finite R₁ B
inst_53 : Algebra.IsSeparable.{u_1, u_2} (FractionRing A) (FractionRing B)
inst_54 : IsScalarTower A R₁ B
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
h₃ :
  IsCoprime.{u_2} (R := Ideal B) (Ideal.map (F := R₁ →+* B) (algebraMap R₁ B) (differentIdeal A R₁))
    (Ideal.map (F := R₂ →+* B) (algebraMap R₂ B) (differentIdeal A R₂))
inst_55 : Free A R₂
B₁ : Basis.{u_6, u_5, u_2} (Free.ChooseBasisIndex A R₂) R₁ B :=
  Basis.ofIsCoprimeDifferentIdeal A B R₁ R₂ h₁ h₂ h₃ (Free.chooseBasis A R₂)
⊢ Eq (α := Subalgebra A B) (AlgHom.range (IsScalarTower.toAlgHom A R₁ B) ⊔ AlgHom.range (IsScalarTower.toAlgHom A R₂ B))
    ⊤
have refine : ∀ (x : B),
  Membership.mem (γ := Subalgebra A B)
    (AlgHom.range (IsScalarTower.toAlgHom A R₁ B) ⊔ AlgHom.range (IsScalarTower.toAlgHom A R₂ B)) x
Tactic: refine Algebra.eq_top_iff.mpr fun x ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.LinearDisjoint (goal)
Goal:
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : CommRing B
inst_5 : Field L
inst_6 : Algebra B L
inst_7 : Algebra A L
inst_8 : Algebra K L
inst_9 : FiniteDimensional K L
inst_10 : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst_11 : CommRing R₁
inst_12 : CommRing R₂
inst_13 : IsDomain R₁
inst_14 : Algebra A R₁
inst_15 : Algebra A R₂
inst_16 : Algebra R₁ B
inst_17 : Algebra R₂ B
inst_18 : Algebra R₁ L
inst_19 : Algebra R₂ L
inst_20 : IsScalarTower A R₁ L
inst_21 : IsScalarTower R₁ B L
inst_22 : IsScalarTower R₂ B L
inst_23 : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst_24 : Algebra.{u_5, u_4} R₁ ↥F₁
inst_25 : Algebra.{u_6, u_4} R₂ ↥F₂
inst_26 : IsTorsionFree.{u_5, u_4} R₁ ↥F₁
inst_27 : IsScalarTower A (↥F₂) L
inst_28 : IsScalarTower.{u_1, u_6, u_4} A R₂ ↥F₂
inst_29 : IsScalarTower R₁ (↥F₁) L
inst_30 : IsScalarTower R₂ (↥F₂) L
inst_31 : Algebra.IsSeparable.{u_3, u_4} K ↥F₂
inst_32 : Algebra.IsSeparable (↥F₁) L
inst_33 : IsDomain A
inst_34 : IsDedekindDomain B
inst_35 : IsDedekindDomain R₁
inst_36 : IsDedekindDomain R₂
inst_37 : IsFractionRing B L
inst_38 : IsFractionRing.{u_5, u_4} R₁ ↥F₁
inst_39 : IsFractionRing.{u_6, u_4} R₂ ↥F₂
inst_40 : IsIntegrallyClosed A
inst_41 : IsIntegralClosure B R₁ L
inst_42 : IsTorsionFree R₁ B
inst_43 : IsTorsionFree R₂ B
inst_44 : Algebra A B
inst_45 : Module.Finite A B
inst_46 : IsTorsionFree A B
inst_47 : IsTorsionFree A R₁
inst_48 : IsTorsionFree A R₂
inst_49 : Module.Finite A R₁
inst_50 : Module.Finite R₂ B
inst_51 : IsScalarTower A R₂ B
inst_52 : Module.Finite R₁ B
inst_53 : Algebra.IsSeparable.{u_1, u_2} (FractionRing A) (FractionRing B)
inst_54 : IsScalarTower A R₁ B
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
h₃ :
  IsCoprime.{u_2} (R := Ideal B) (Ideal.map (F := R₁ →+* B) (algebraMap R₁ B) (differentIdeal A R₁))
    (Ideal.map (F := R₂ →+* B) (algebraMap R₂ B) (differentIdeal A R₂))
inst_55 : Free A R₂
B₁ : Basis.{u_6, u_5, u_2} (Free.ChooseBasisIndex A R₂) R₁ B :=
  Basis.ofIsCoprimeDifferentIdeal A B R₁ R₂ h₁ h₂ h₃ (Free.chooseBasis A R₂)
x : B
⊢ Membership.mem (γ := Subalgebra A B)
    (AlgHom.range (IsScalarTower.toAlgHom A R₁ B) ⊔ AlgHom.range (IsScalarTower.toAlgHom A R₂ B)) x
have rw : Membership.mem (γ := Subalgebra A B)
  (AlgHom.range (IsScalarTower.toAlgHom A R₁ B) ⊔ AlgHom.range (IsScalarTower.toAlgHom A R₂ B))
  (∑ i : Free.ChooseBasisIndex A R₂,
    HSMul.hSMul.{u_5, u_2, u_2} (α := R₁) (β := B)
      ((((B₁.repr : (a : B) → Free.ChooseBasisIndex A R₂ →₀ R₁) x :
              Finsupp.{u_6, u_5} (Free.ChooseBasisIndex A R₂) R₁) :
            (a : Free.ChooseBasisIndex A R₂) → R₁)
          i :
        R₁)
      ((B₁ : (a : Free.ChooseBasisIndex A R₂) → B) i : B))
Tactic: rw [← B₁.sum_repr x]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.LinearDisjoint (goal)
Goal:
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : CommRing B
inst_5 : Field L
inst_6 : Algebra B L
inst_7 : Algebra A L
inst_8 : Algebra K L
inst_9 : FiniteDimensional K L
inst_10 : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst_11 : CommRing R₁
inst_12 : CommRing R₂
inst_13 : IsDomain R₁
inst_14 : Algebra A R₁
inst_15 : Algebra A R₂
inst_16 : Algebra R₁ B
inst_17 : Algebra R₂ B
inst_18 : Algebra R₁ L
inst_19 : Algebra R₂ L
inst_20 : IsScalarTower A R₁ L
inst_21 : IsScalarTower R₁ B L
inst_22 : IsScalarTower R₂ B L
inst_23 : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst_24 : Algebra.{u_5, u_4} R₁ ↥F₁
inst_25 : Algebra.{u_6, u_4} R₂ ↥F₂
inst_26 : IsTorsionFree.{u_5, u_4} R₁ ↥F₁
inst_27 : IsScalarTower A (↥F₂) L
inst_28 : IsScalarTower.{u_1, u_6, u_4} A R₂ ↥F₂
inst_29 : IsScalarTower R₁ (↥F₁) L
inst_30 : IsScalarTower R₂ (↥F₂) L
inst_31 : Algebra.IsSeparable.{u_3, u_4} K ↥F₂
inst_32 : Algebra.IsSeparable (↥F₁) L
inst_33 : IsDomain A
inst_34 : IsDedekindDomain B
inst_35 : IsDedekindDomain R₁
inst_36 : IsDedekindDomain R₂
inst_37 : IsFractionRing B L
inst_38 : IsFractionRing.{u_5, u_4} R₁ ↥F₁
inst_39 : IsFractionRing.{u_6, u_4} R₂ ↥F₂
inst_40 : IsIntegrallyClosed A
inst_41 : IsIntegralClosure B R₁ L
inst_42 : IsTorsionFree R₁ B
inst_43 : IsTorsionFree R₂ B
inst_44 : Algebra A B
inst_45 : Module.Finite A B
inst_46 : IsTorsionFree A B
inst_47 : IsTorsionFree A R₁
inst_48 : IsTorsionFree A R₂
inst_49 : Module.Finite A R₁
inst_50 : Module.Finite R₂ B
inst_51 : IsScalarTower A R₂ B
inst_52 : Module.Finite R₁ B
inst_53 : Algebra.IsSeparable.{u_1, u_2} (FractionRing A) (FractionRing B)
inst_54 : IsScalarTower A R₁ B
inst_55 : Free A R₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
h₃ :
  IsCoprime.{u_2} (R := Ideal B) (Ideal.map (F := R₁ →+* B) (algebraMap R₁ B) (differentIdeal A R₁))
    (Ideal.map (F := R₂ →+* B) (algebraMap R₂ B) (differentIdeal A R₂))
s : Set R₁
t : Set R₂
hs : Eq (α := Subalgebra A R₁) (Algebra.adjoin A s) ⊤
ht : Eq (α := Subalgebra A R₂) (Algebra.adjoin A t) ⊤
⊢ Eq.{u_2 + 1} (α := Subalgebra A B)
    (Algebra.adjoin A ((⇑(algebraMap R₁ B) : (a : R₁) → B) '' s ∪ (⇑(algebraMap R₂ B) : (a : R₂) → B) '' t)) ⊤
have rw : Eq (α := Subalgebra A B) (AlgHom.range (IsScalarTower.toAlgHom A R₁ B) ⊔ AlgHom.range (IsScalarTower.toAlgHom A R₂ B)) ⊤
Tactic: rw [Algebra.adjoin_union, ← IsScalarTower.coe_toAlgHom' A R₁, ← IsScalarTower.coe_toAlgHom' A R₂,
    ← AlgHom.map_adjoin, hs, ← AlgHom.map_adjoin, ht, Algebra.map_top, Algebra.map_top]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
⊢ P = span {x}
have pos : ∀ (hP0 : P = ⊥), P = span {x}
Tactic: by_cases hP0 : P = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
pos : ∀ (hP0 : P = ⊥), P = span {x}
⊢ P = span {x}
have neg : ∀ (hP0 : ¬P = ⊥), P = span {x}
Tactic: by_cases hP0 : P = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : P = ⊥
⊢ P = span {x}
have pos : ∀ (hP : IsPrime.{u_1} (α := R) ⊥) (x_mem : Membership.mem (γ := Ideal R) ⊥ x)
  (hxP2 : x ∉ HPow.hPow (α := Ideal R) (β := ℕ) ⊥ 2) (hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ ⊥ → x ∉ Q),
  Eq (α := Ideal R) ⊥ (span {x})
Tactic: subst hP0
Cleared hypotheses: P, hP, x_mem, hxP2, hxQ, hP0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
x : R
hP : IsPrime.{u_1} (α := R) ⊥
x_mem : Membership.mem (γ := Ideal R) ⊥ x
hxP2 : x ∉ HPow.hPow (α := Ideal R) (β := ℕ) ⊥ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ ⊥ → x ∉ Q
⊢ Eq (α := Ideal R) ⊥ (span {x})
have pos : Eq (α := Ideal R) (span {x}) ⊥
Tactic: rwa [eq_comm, span_singleton_eq_bot, ← mem_bot]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
x : R
hP : IsPrime.{u_1} (α := R) ⊥
x_mem : Membership.mem (γ := Ideal R) ⊥ x
hxP2 : x ∉ HPow.hPow (α := Ideal R) (β := ℕ) ⊥ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ ⊥ → x ∉ Q
pos : Eq (α := Ideal R) (span {x}) ⊥
⊢ Eq (α := Ideal R) ⊥ (span {x})
have pos₁ : x = 0
Tactic: rwa [eq_comm, span_singleton_eq_bot, ← mem_bot]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
⊢ P = span {x}
have hspan0 : Ne (α := Ideal R) (span {x}) ⊥
Tactic: have hspan0 : span {x} ≠ ⊥ := mt Ideal.span_singleton_eq_bot.mp (hxP2 <| · ▸ zero_mem _)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
⊢ P = span {x}
have neg : normalizedFactors P = normalizedFactors (span {x})
Tactic: rw [← associated_iff_eq, associated_iff_normalizedFactors_eq_normalizedFactors hP0 hspan0]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
⊢ normalizedFactors P = normalizedFactors (span {x})
have neg : ∀ (Q : Ideal R), Multiset.count Q (normalizedFactors P) = Multiset.count Q (normalizedFactors (span {x}))
Tactic: refine Multiset.ext' fun Q ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
Q : Ideal R
⊢ Multiset.count Q (normalizedFactors P) = Multiset.count Q (normalizedFactors (span {x}))
have neg : (if Q = P then 1 else 0) = Multiset.count Q (normalizedFactors (span {x}))
Tactic: rw [normalizedFactors_irreducible (Ideal.prime_of_isPrime hP0 hP).irreducible, normalize_eq,
    Multiset.count_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
Q : Ideal R
⊢ (if Q = P then 1 else 0) = Multiset.count Q (normalizedFactors (span {x}))
have neg : Multiset.count Q (normalizedFactors (span {x})) = if Q = P then 1 else 0
Tactic: symm
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
Q : Ideal R
⊢ Multiset.count Q (normalizedFactors (span {x})) = if Q = P then 1 else 0
have pos : ∀ (hQ : Q = P), Multiset.count Q (normalizedFactors (span {x})) = 1
Tactic: split_ifs with hQ
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
Q : Ideal R
pos : ∀ (hQ : Q = P), Multiset.count Q (normalizedFactors (span {x})) = 1
⊢ Multiset.count Q (normalizedFactors (span {x})) = if Q = P then 1 else 0
have neg : ∀ (hQ : ¬Q = P), Multiset.count Q (normalizedFactors (span {x})) = 0
Tactic: split_ifs with hQ
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
Q : Ideal R
hQ : Q = P
⊢ Multiset.count Q (normalizedFactors (span {x})) = 1
have hP₁ : Q.IsPrime
Tactic: subst hQ
Cleared hypotheses: P, hP, x_mem, hxP2, hxQ, hP0, hQ
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
Q : Ideal R
hQ : Q = P
hP₁ : Q.IsPrime
⊢ Multiset.count Q (normalizedFactors (span {x})) = 1
have x_mem₁ : x ∈ Q
Tactic: subst hQ
Cleared hypotheses: P, hP, x_mem, hxP2, hxQ, hP0, hQ
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
hP : P.IsPrime
inst_1 : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ HPow.hPow (β := ℕ) P 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : Ne (α := Ideal R) (span {x}) ⊥
Q : Ideal R
hQ : Q = P
hP₁ : Q.IsPrime
x_mem₁ : x ∈ Q
⊢ Multiset.count Q (normalizedFactors (span {x})) = 1
have hxP2₁ : x ∉ HPow.hPow (β := ℕ) Q 2
Tactic: subst hQ
Cleared hypotheses: P, hP, x_mem, hxP2, hxQ, hP0, hQ