awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this_2 : IsTorsionFree A L
this : IsTorsionFree A C
⊢ IsLocalization (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) L
have refine_1 : ∀ (y : ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)),
  IsUnit.{u_3} (M := L) ((algebraMap C L : (a : C) → L) (↑y : C) : L)
Tactic: refine ⟨?_, fun z => ?_, fun {x y} h => ⟨1, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this_2 : IsTorsionFree A L
this : IsTorsionFree A C
refine_1 :
  ∀ (y : ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)),
    IsUnit.{u_3} (M := L) ((algebraMap C L : (a : C) → L) (↑y : C) : L)
⊢ IsLocalization (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) L
have refine_2 : ∀ (z : L),
  ∃ (x : C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)),
    HMul.hMul (β := L) z ((algebraMap C L : (a : C) → L) (↑x.2 : C) : L) = (algebraMap C L : (a : C) → L) x.1
Tactic: refine ⟨?_, fun z => ?_, fun {x y} h => ⟨1, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this_2 : IsTorsionFree A L
this : IsTorsionFree A C
refine_1 :
  ∀ (y : ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)),
    IsUnit.{u_3} (M := L) ((algebraMap C L : (a : C) → L) (↑y : C) : L)
refine_2 :
  ∀ (z : L),
    ∃ (x : C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)),
      HMul.hMul (β := L) z ((algebraMap C L : (a : C) → L) (↑x.2 : C) : L) = (algebraMap C L : (a : C) → L) x.1
⊢ IsLocalization (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) L
have refine_3 : ∀ {x y : C} (h : Eq.{u_3 + 1} (α := L) ((algebraMap C L : (a : C) → L) x : L) ((algebraMap C L : (a : C) → L) y : L)),
  (↑1 : C) * x = (↑1 : C) * y
Tactic: refine ⟨?_, fun z => ?_, fun {x y} h => ⟨1, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this_2 : IsTorsionFree A L
this : IsTorsionFree A C
x : A
hx : x ∈ (↑(A⁰ : Submonoid A) : Set A)
⊢ IsUnit.{u_3} (M := L)
    ((algebraMap C L : (a : C) → L)
        ((↑(Subtype.mk (p := fun (x : C) ↦
                Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
                ((algebraMap A C : (a : A) → C) x) ⋯) :
            C) :
          C) :
      L)
have refine_1 : x ≠ 0
Tactic: rw [isUnit_iff_ne_zero, map_ne_zero_iff _ (IsIntegralClosure.algebraMap_injective C A L),
      Subtype.coe_mk, map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective A C)]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this_2 : IsTorsionFree A L
this : IsTorsionFree A C
z : L
⊢ ∃ (x : C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)),
    HMul.hMul (β := L) z ((algebraMap C L : (a : C) → L) (↑x.2 : C) : L) = (algebraMap C L : (a : C) → L) x.1
have refine_2 : ∀ (m : ↥(A⁰ : Submonoid A)) (hm : IsIntegral A (m • z)),
  ∃ (x : C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)),
    HMul.hMul (β := L) z ((algebraMap C L : (a : C) → L) (↑x.2 : C) : L) = (algebraMap C L : (a : C) → L) x.1
Tactic: obtain ⟨m, hm⟩ :=
      IsIntegral.exists_multiple_integral_of_isLocalization A⁰ z
        (Algebra.IsIntegral.isIntegral (R := K) z)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this_2 : IsTorsionFree A L
this : IsTorsionFree A C
z : L
m : ↥(A⁰ : Submonoid A)
hm : IsIntegral A (m • z)
⊢ ∃ (x : C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)),
    HMul.hMul (β := L) z ((algebraMap C L : (a : C) → L) (↑x.2 : C) : L) = (algebraMap C L : (a : C) → L) x.1
have refine_2 : ∀ (x : C) (hx : (algebraMap C L : (a : C) → L) x = m • z),
  ∃ (x : C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)),
    HMul.hMul (β := L) z ((algebraMap C L : (a : C) → L) (↑x.2 : C) : L) = (algebraMap C L : (a : C) → L) x.1
Tactic: obtain ⟨x, hx⟩ : ∃ x, algebraMap C L x = m • z := IsIntegralClosure.isIntegral_iff.mp hm
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this_2 : IsTorsionFree A L
this : IsTorsionFree A C
z : L
m : ↥(A⁰ : Submonoid A)
hm : IsIntegral A (m • z)
x : C
hx : (algebraMap C L : (a : C) → L) x = m • z
⊢ ∃ (x : C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)),
    HMul.hMul (β := L) z ((algebraMap C L : (a : C) → L) (↑x.2 : C) : L) = (algebraMap C L : (a : C) → L) x.1
have refine_2 : HMul.hMul (β := L) z
    ((algebraMap C L : (a : C) → L)
        ((↑(x,
                  Subtype.mk (p := fun (x : C) ↦
                    Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
                    ((algebraMap A C : (a : A) → C) (↑m : A)) sorry).2 :
            C) :
          C) :
      L) =
  (algebraMap C L : (a : C) → L)
    ((x,
          Subtype.mk (p := fun (x : C) ↦
            Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
            ((algebraMap A C : (a : A) → C) (↑m : A)) sorry) :
        C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)).1
Tactic: refine ⟨⟨x, algebraMap A C m, m, SetLike.coe_mem m, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this_2 : IsTorsionFree A L
this : IsTorsionFree A C
z : L
m : ↥(A⁰ : Submonoid A)
hm : IsIntegral A (m • z)
x : C
hx : (algebraMap C L : (a : C) → L) x = m • z
⊢ HMul.hMul (β := L) z
      ((algebraMap C L : (a : C) → L)
          ((↑(x,
                    Subtype.mk (p := fun (x : C) ↦
                      Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
                      ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯).2 :
              C) :
            C) :
        L) =
    (algebraMap C L : (a : C) → L)
      ((x,
            Subtype.mk (p := fun (x : C) ↦
              Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
              ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯) :
          C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)).1
have refine_2 : HMul.hMul (β := L) z ((algebraMap C L : (a : C) → L) ((algebraMap A C : (a : A) → C) (↑m : A) : C) : L) =
  (algebraMap C L : (a : C) → L)
    ((x,
          Subtype.mk (p := fun (x : C) ↦
            Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
            ((algebraMap A C : (a : A) → C) (↑m : A)) sorry) :
        C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)).1
Tactic: rw [Subtype.coe_mk, ← IsScalarTower.algebraMap_apply, hx, mul_comm, Submonoid.smul_def,
      smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this_2 : IsTorsionFree A L
this : IsTorsionFree A C
z : L
m : ↥(A⁰ : Submonoid A)
hm : IsIntegral A (m • z)
x : C
hx : (algebraMap C L : (a : C) → L) x = m • z
refine_2 :
  HMul.hMul (β := L) z ((algebraMap C L : (a : C) → L) ((algebraMap A C : (a : A) → C) (↑m : A) : C) : L) =
    (algebraMap C L : (a : C) → L)
      ((x,
            Subtype.mk (p := fun (x : C) ↦
              Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
              ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯) :
          C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)).1
⊢ HMul.hMul (β := L) z
      ((algebraMap C L : (a : C) → L)
          ((↑(x,
                    Subtype.mk (p := fun (x : C) ↦
                      Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
                      ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯).2 :
              C) :
            C) :
        L) =
    (algebraMap C L : (a : C) → L)
      ((x,
            Subtype.mk (p := fun (x : C) ↦
              Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
              ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯) :
          C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)).1
have refine_2₁ : HMul.hMul (β := L) z ((algebraMap A L : (a : A) → L) (↑m : A) : L) =
  (algebraMap C L : (a : C) → L)
    ((x,
          Subtype.mk (p := fun (x : C) ↦
            Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
            ((algebraMap A C : (a : A) → C) (↑m : A)) sorry) :
        C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)).1
Tactic: rw [Subtype.coe_mk, ← IsScalarTower.algebraMap_apply, hx, mul_comm, Submonoid.smul_def,
      smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this_2 : IsTorsionFree A L
this : IsTorsionFree A C
z : L
m : ↥(A⁰ : Submonoid A)
hm : IsIntegral A (m • z)
x : C
hx : (algebraMap C L : (a : C) → L) x = m • z
refine_2 :
  HMul.hMul (β := L) z ((algebraMap C L : (a : C) → L) ((algebraMap A C : (a : A) → C) (↑m : A) : C) : L) =
    (algebraMap C L : (a : C) → L)
      ((x,
            Subtype.mk (p := fun (x : C) ↦
              Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
              ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯) :
          C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)).1
refine_2₁ :
  HMul.hMul (β := L) z ((algebraMap A L : (a : A) → L) (↑m : A) : L) =
    (algebraMap C L : (a : C) → L)
      ((x,
            Subtype.mk (p := fun (x : C) ↦
              Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
              ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯) :
          C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)).1
⊢ HMul.hMul (β := L) z
      ((algebraMap C L : (a : C) → L)
          ((↑(x,
                    Subtype.mk (p := fun (x : C) ↦
                      Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
                      ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯).2 :
              C) :
            C) :
        L) =
    (algebraMap C L : (a : C) → L)
      ((x,
            Subtype.mk (p := fun (x : C) ↦
              Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
              ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯) :
          C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)).1
have refine_2₂ : HMul.hMul (β := L) z ((algebraMap A L : (a : A) → L) (↑m : A) : L) = m • z
Tactic: rw [Subtype.coe_mk, ← IsScalarTower.algebraMap_apply, hx, mul_comm, Submonoid.smul_def,
      smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this_2 : IsTorsionFree A L
this : IsTorsionFree A C
z : L
m : ↥(A⁰ : Submonoid A)
hm : IsIntegral A (m • z)
x : C
hx : (algebraMap C L : (a : C) → L) x = m • z
refine_2 :
  HMul.hMul (β := L) z ((algebraMap C L : (a : C) → L) ((algebraMap A C : (a : A) → C) (↑m : A) : C) : L) =
    (algebraMap C L : (a : C) → L)
      ((x,
            Subtype.mk (p := fun (x : C) ↦
              Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
              ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯) :
          C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)).1
refine_2₁ :
  HMul.hMul (β := L) z ((algebraMap A L : (a : A) → L) (↑m : A) : L) =
    (algebraMap C L : (a : C) → L)
      ((x,
            Subtype.mk (p := fun (x : C) ↦
              Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
              ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯) :
          C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)).1
refine_2₂ : HMul.hMul (β := L) z ((algebraMap A L : (a : A) → L) (↑m : A) : L) = m • z
⊢ HMul.hMul (β := L) z
      ((algebraMap C L : (a : C) → L)
          ((↑(x,
                    Subtype.mk (p := fun (x : C) ↦
                      Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
                      ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯).2 :
              C) :
            C) :
        L) =
    (algebraMap C L : (a : C) → L)
      ((x,
            Subtype.mk (p := fun (x : C) ↦
              Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
              ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯) :
          C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)).1
have refine_2₃ : HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) (↑m : A) : L) z = m • z
Tactic: rw [Subtype.coe_mk, ← IsScalarTower.algebraMap_apply, hx, mul_comm, Submonoid.smul_def,
      smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this_2 : IsTorsionFree A L
this : IsTorsionFree A C
z : L
m : ↥(A⁰ : Submonoid A)
hm : IsIntegral A (m • z)
x : C
hx : (algebraMap C L : (a : C) → L) x = m • z
refine_2 :
  HMul.hMul (β := L) z ((algebraMap C L : (a : C) → L) ((algebraMap A C : (a : A) → C) (↑m : A) : C) : L) =
    (algebraMap C L : (a : C) → L)
      ((x,
            Subtype.mk (p := fun (x : C) ↦
              Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
              ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯) :
          C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)).1
refine_2₁ :
  HMul.hMul (β := L) z ((algebraMap A L : (a : A) → L) (↑m : A) : L) =
    (algebraMap C L : (a : C) → L)
      ((x,
            Subtype.mk (p := fun (x : C) ↦
              Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
              ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯) :
          C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)).1
refine_2₂ : HMul.hMul (β := L) z ((algebraMap A L : (a : A) → L) (↑m : A) : L) = m • z
refine_2₃ : HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) (↑m : A) : L) z = m • z
⊢ HMul.hMul (β := L) z
      ((algebraMap C L : (a : C) → L)
          ((↑(x,
                    Subtype.mk (p := fun (x : C) ↦
                      Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
                      ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯).2 :
              C) :
            C) :
        L) =
    (algebraMap C L : (a : C) → L)
      ((x,
            Subtype.mk (p := fun (x : C) ↦
              Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
              ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯) :
          C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)).1
have refine_2₄ : HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) (↑m : A) : L) z = (↑m : A) • z
Tactic: rw [Subtype.coe_mk, ← IsScalarTower.algebraMap_apply, hx, mul_comm, Submonoid.smul_def,
      smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this_2 : IsTorsionFree A L
this : IsTorsionFree A C
z : L
m : ↥(A⁰ : Submonoid A)
hm : IsIntegral A (m • z)
x : C
hx : (algebraMap C L : (a : C) → L) x = m • z
refine_2 :
  HMul.hMul (β := L) z ((algebraMap C L : (a : C) → L) ((algebraMap A C : (a : A) → C) (↑m : A) : C) : L) =
    (algebraMap C L : (a : C) → L)
      ((x,
            Subtype.mk (p := fun (x : C) ↦
              Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
              ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯) :
          C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)).1
refine_2₁ :
  HMul.hMul (β := L) z ((algebraMap A L : (a : A) → L) (↑m : A) : L) =
    (algebraMap C L : (a : C) → L)
      ((x,
            Subtype.mk (p := fun (x : C) ↦
              Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
              ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯) :
          C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)).1
refine_2₂ : HMul.hMul (β := L) z ((algebraMap A L : (a : A) → L) (↑m : A) : L) = m • z
refine_2₃ : HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) (↑m : A) : L) z = m • z
refine_2₄ : HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) (↑m : A) : L) z = (↑m : A) • z
⊢ HMul.hMul (β := L) z
      ((algebraMap C L : (a : C) → L)
          ((↑(x,
                    Subtype.mk (p := fun (x : C) ↦
                      Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
                      ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯).2 :
              C) :
            C) :
        L) =
    (algebraMap C L : (a : C) → L)
      ((x,
            Subtype.mk (p := fun (x : C) ↦
              Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
              ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯) :
          C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)).1
have refine_2₅ : HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) (↑m : A) : L) z =
  HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) (↑m : A) : L) z
Tactic: rw [Subtype.coe_mk, ← IsScalarTower.algebraMap_apply, hx, mul_comm, Submonoid.smul_def,
      smul_def]