awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
n : ℕ
inst_5 : CharZero S
this_1 :
  Finite.{max 1 (u_1 + 1)}
    { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }
this : Finite.{max 1 (u_1 + 1)} { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }
e : { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } ≃
  { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n } ⊕
    { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n } :=
  Equiv.trans
    (Equiv.subtypeEquivRight (p := fun (I : Ideal S) ↦ (absNorm : (a : Ideal S) → ℕ) I ≤ n) (q := fun (x : Ideal S) ↦
      Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n ∨
        x ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n)
      ⋯)
    (subtypeOrEquiv
      (fun (I : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n)
      (fun (I : Ideal S) ↦ I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n) ⋯)
⊢ Nat.card.{u_1} { I : Ideal S // I = ⊥ } = 1
have rw : Eq (α := ℕ) 1 1
Tactic: rw [Nat.card_unique]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
n : ℕ
inst_5 : CharZero S
⊢ Nat.card.{u_1} { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } =
    Nat.card.{u_1} { I : ↥(Ideal S)⁰ // (absNorm : (a : Ideal S) → ℕ) (↑I : Ideal S) ≤ n } + 1
have have : ∀
  (this :
    Finite.{max 1 (u_1 + 1)}
      { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }),
  Nat.card.{u_1} { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } =
    Nat.card.{u_1} { I : ↥(Ideal S)⁰ // (absNorm : (a : Ideal S) → ℕ) (↑I : Ideal S) ≤ n } + 1
Tactic: classical
  have : Finite {I : Ideal S // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n} :=
    (finite_setOf_absNorm_le n).subset fun _ ⟨_, h⟩ ↦ h
  have : Finite {I : Ideal S // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n} :=
    (finite_setOf_absNorm_le n).subset fun _ ⟨_, h⟩ ↦ h
  rw [Nat.card_congr (Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ I ∈ (Ideal S)⁰)
    (fun I ↦ absNorm I ≤ n))]
  let e : {I : Ideal S // absNorm I ≤ n} ≃ {I : Ideal S // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n} ⊕
      {I : Ideal S // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n} := by
    refine (Equiv.subtypeEquivRight ?_).trans (subtypeOrEquiv _ _ ?_)
    · intro _
      simp_rw [← or_and_right, em, true_and]
    · exact Pi.disjoint_iff.mpr fun I ↦ Prop.disjoint_iff.mpr (by tauto)
  simp_rw [Nat.card_congr e, Nat.card_sum, add_right_inj]
  conv_lhs =>
    enter [1, 1, I]
    rw [← absNorm_ne_zero_iff_mem_nonZeroDivisors, ne_eq, not_not, and_iff_left_iff_imp.mpr
      (fun h ↦ by rw [h]; exact Nat.zero_le n), absNorm_eq_zero_iff]
  rw [Nat.card_unique]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
n : ℕ
inst_5 : CharZero S
have have₁ have₂ :
  ∀
    (this :
      Finite.{max 1 (u_1 + 1)}
        { I : Ideal S //
          Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }),
    Nat.card.{u_1} { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } =
      Nat.card.{u_1} { I : ↥(Ideal S)⁰ // (absNorm : (a : Ideal S) → ℕ) (↑I : Ideal S) ≤ n } + 1
⊢ Nat.card.{u_1} { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } =
    Nat.card.{u_1} { I : ↥(Ideal S)⁰ // (absNorm : (a : Ideal S) → ℕ) (↑I : Ideal S) ≤ n } + 1
have have₃ : ∀
  (this :
    Finite.{max 1 (u_1 + 1)}
      { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n })
  (this : Finite.{max 1 (u_1 + 1)} { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }),
  Nat.card.{u_1} { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } =
    Nat.card.{u_1} { I : ↥(Ideal S)⁰ // (absNorm : (a : Ideal S) → ℕ) (↑I : Ideal S) ≤ n } + 1
Tactic: classical
  have : Finite {I : Ideal S // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n} :=
    (finite_setOf_absNorm_le n).subset fun _ ⟨_, h⟩ ↦ h
  have : Finite {I : Ideal S // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n} :=
    (finite_setOf_absNorm_le n).subset fun _ ⟨_, h⟩ ↦ h
  rw [Nat.card_congr (Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ I ∈ (Ideal S)⁰)
    (fun I ↦ absNorm I ≤ n))]
  let e : {I : Ideal S // absNorm I ≤ n} ≃ {I : Ideal S // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n} ⊕
      {I : Ideal S // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n} := by
    refine (Equiv.subtypeEquivRight ?_).trans (subtypeOrEquiv _ _ ?_)
    · intro _
      simp_rw [← or_and_right, em, true_and]
    · exact Pi.disjoint_iff.mpr fun I ↦ Prop.disjoint_iff.mpr (by tauto)
  simp_rw [Nat.card_congr e, Nat.card_sum, add_right_inj]
  conv_lhs =>
    enter [1, 1, I]
    rw [← absNorm_ne_zero_iff_mem_nonZeroDivisors, ne_eq, not_not, and_iff_left_iff_imp.mpr
      (fun h ↦ by rw [h]; exact Nat.zero_le n), absNorm_eq_zero_iff]
  rw [Nat.card_unique]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
n : ℕ
inst_5 : CharZero S
have have₁ have₂ :
  ∀
    (this :
      Finite.{max 1 (u_1 + 1)}
        { I : Ideal S //
          Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }),
    Nat.card.{u_1} { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } =
      Nat.card.{u_1} { I : ↥(Ideal S)⁰ // (absNorm : (a : Ideal S) → ℕ) (↑I : Ideal S) ≤ n } + 1
have₃ :
  ∀
    (this :
      Finite.{max 1 (u_1 + 1)}
        { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n })
    (this : Finite.{max 1 (u_1 + 1)} { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }),
    Nat.card.{u_1} { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } =
      Nat.card.{u_1} { I : ↥(Ideal S)⁰ // (absNorm : (a : Ideal S) → ℕ) (↑I : Ideal S) ≤ n } + 1
⊢ Nat.card.{u_1} { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } =
    Nat.card.{u_1} { I : ↥(Ideal S)⁰ // (absNorm : (a : Ideal S) → ℕ) (↑I : Ideal S) ≤ n } + 1
have have₄ : ∀
  (this :
    Finite.{max 1 (u_1 + 1)}
      { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n })
  (this : Finite.{max 1 (u_1 + 1)} { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }),
  Nat.card.{u_1} { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } =
    Nat.card.{u_1}
        { x : Ideal S //
          Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n } +
      1
Tactic: classical
  have : Finite {I : Ideal S // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n} :=
    (finite_setOf_absNorm_le n).subset fun _ ⟨_, h⟩ ↦ h
  have : Finite {I : Ideal S // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n} :=
    (finite_setOf_absNorm_le n).subset fun _ ⟨_, h⟩ ↦ h
  rw [Nat.card_congr (Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ I ∈ (Ideal S)⁰)
    (fun I ↦ absNorm I ≤ n))]
  let e : {I : Ideal S // absNorm I ≤ n} ≃ {I : Ideal S // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n} ⊕
      {I : Ideal S // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n} := by
    refine (Equiv.subtypeEquivRight ?_).trans (subtypeOrEquiv _ _ ?_)
    · intro _
      simp_rw [← or_and_right, em, true_and]
    · exact Pi.disjoint_iff.mpr fun I ↦ Prop.disjoint_iff.mpr (by tauto)
  simp_rw [Nat.card_congr e, Nat.card_sum, add_right_inj]
  conv_lhs =>
    enter [1, 1, I]
    rw [← absNorm_ne_zero_iff_mem_nonZeroDivisors, ne_eq, not_not, and_iff_left_iff_imp.mpr
      (fun h ↦ by rw [h]; exact Nat.zero_le n), absNorm_eq_zero_iff]
  rw [Nat.card_unique]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
n : ℕ
inst_5 : CharZero S
have have₁ have₂ :
  ∀
    (this :
      Finite.{max 1 (u_1 + 1)}
        { I : Ideal S //
          Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }),
    Nat.card.{u_1} { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } =
      Nat.card.{u_1} { I : ↥(Ideal S)⁰ // (absNorm : (a : Ideal S) → ℕ) (↑I : Ideal S) ≤ n } + 1
have₃ :
  ∀
    (this :
      Finite.{max 1 (u_1 + 1)}
        { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n })
    (this : Finite.{max 1 (u_1 + 1)} { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }),
    Nat.card.{u_1} { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } =
      Nat.card.{u_1} { I : ↥(Ideal S)⁰ // (absNorm : (a : Ideal S) → ℕ) (↑I : Ideal S) ≤ n } + 1
have₄ have₅ :
  ∀
    (this :
      Finite.{max 1 (u_1 + 1)}
        { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n })
    (this : Finite.{max 1 (u_1 + 1)} { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }),
    Nat.card.{u_1} { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } =
      Nat.card.{u_1}
          { x : Ideal S //
            Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n } +
        1
⊢ Nat.card.{u_1} { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } =
    Nat.card.{u_1} { I : ↥(Ideal S)⁰ // (absNorm : (a : Ideal S) → ℕ) (↑I : Ideal S) ≤ n } + 1
have have₆ : ∀
  (this :
    Finite.{max 1 (u_1 + 1)}
      { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n })
  (this : Finite.{max 1 (u_1 + 1)} { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }),
  Nat.card.{u_1} { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n } = 1
Tactic: classical
  have : Finite {I : Ideal S // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n} :=
    (finite_setOf_absNorm_le n).subset fun _ ⟨_, h⟩ ↦ h
  have : Finite {I : Ideal S // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n} :=
    (finite_setOf_absNorm_le n).subset fun _ ⟨_, h⟩ ↦ h
  rw [Nat.card_congr (Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ I ∈ (Ideal S)⁰)
    (fun I ↦ absNorm I ≤ n))]
  let e : {I : Ideal S // absNorm I ≤ n} ≃ {I : Ideal S // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n} ⊕
      {I : Ideal S // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n} := by
    refine (Equiv.subtypeEquivRight ?_).trans (subtypeOrEquiv _ _ ?_)
    · intro _
      simp_rw [← or_and_right, em, true_and]
    · exact Pi.disjoint_iff.mpr fun I ↦ Prop.disjoint_iff.mpr (by tauto)
  simp_rw [Nat.card_congr e, Nat.card_sum, add_right_inj]
  conv_lhs =>
    enter [1, 1, I]
    rw [← absNorm_ne_zero_iff_mem_nonZeroDivisors, ne_eq, not_not, and_iff_left_iff_imp.mpr
      (fun h ↦ by rw [h]; exact Nat.zero_le n), absNorm_eq_zero_iff]
  rw [Nat.card_unique]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
x : S
hx : Prime (M := ℤ) ((Algebra.norm ℤ : (a : S) → ℤ) x : ℤ)
y : ℤ
⊢ (Algebra.norm ℤ : (a : S) → ℤ) x ∣ y ↔ x ∣ (↑y : S)
have rw : Nat.Prime ((absNorm : (a : Ideal S) → ℕ) (span {x}))
Tactic: rw [← Ideal.mem_span_singleton (y := x), ← eq_intCast (algebraMap ℤ S), ← Ideal.mem_comap,
    ← Ideal.span_singleton_absNorm, Ideal.mem_span_singleton, Ideal.absNorm_span_singleton,
    Int.natAbs_dvd]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
x : S
hx : Prime (M := ℤ) ((Algebra.norm ℤ : (a : S) → ℤ) x : ℤ)
y : ℤ
⊢ Nat.Prime ((absNorm : (a : Ideal S) → ℕ) (span {x}))
have rwa : Nat.Prime (Int.natAbs ((Algebra.norm ℤ : (a : S) → ℤ) x))
Tactic: rwa [Ideal.absNorm_span_singleton, ← Int.prime_iff_natAbs_prime]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
Goal:
J : Ideal ℤ
⊢ span {(↑((absNorm : (a : Ideal ℤ) → ℕ) J) : ℤ)} = J
have obtain : ∀ (g : ℤ), Eq (α := Ideal ℤ) (span {(↑((absNorm : (a : Ideal ℤ) → ℕ) (ℤ ∙ g)) : ℤ)}) (ℤ ∙ g)
Tactic: obtain ⟨g, rfl⟩ := IsPrincipalIdealRing.principal J
Cleared hypotheses: J
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
Goal:
J : Ideal ℤ
⊢ Nat.Prime ((absNorm : (a : Ideal ℤ) → ℕ) J) ↔ Prime J
have obtain : ∀ (g : ℤ), Nat.Prime ((absNorm : (a : Ideal ℤ) → ℕ) (ℤ ∙ g)) ↔ Prime (M := Ideal ℤ) (ℤ ∙ g)
Tactic: obtain ⟨g, rfl⟩ := IsPrincipalIdealRing.principal J
Cleared hypotheses: J
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : Free R S
I : Ideal S
x : S
hx : x ∈ I
⊢ Membership.mem (α := R) (γ := Ideal R) (spanNorm R I) ((Algebra.norm R : (a : S) → R) x : R)
have refine : Eq.{u_1 + 1} (α := R) ((Algebra.intNorm R S : (a : S) → R) x : R) ((Algebra.norm R : (a : S) → R) x : R)
Tactic: refine subset_span ⟨x, hx, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : Free R S
I : Ideal S
x : S
hx : x ∈ I
⊢ Eq.{u_1 + 1} (α := R) ((Algebra.intNorm R S : (a : S) → R) x : R) ((Algebra.norm R : (a : S) → R) x : R)
have rw : Eq.{u_1 + 1} (α := R) ((Algebra.norm R : (a : S) → R) x : R) ((Algebra.norm R : (a : S) → R) x : R)
Tactic: rw [Algebra.intNorm_eq_norm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
r : S
x : R
hx : Membership.mem (γ := Set R) ((⇑(Algebra.intNorm R S) : (a : S) → R) '' (↑(span {r}) : Set S)) x
⊢ (Algebra.intNorm R S : (a : S) → R) r ∣ x
have obtain : ∀ (x : S) (hx' : x ∈ (↑(span {r}) : Set S))
  (hx :
    Membership.mem.{u_1, u_1} (α := R) (γ := Set R) ((⇑(Algebra.intNorm R S) : (a : S) → R) '' (↑(span {r}) : Set S))
      ((Algebra.intNorm R S : (a : S) → R) x : R)),
  Dvd.dvd.{u_1} (α := R) ((Algebra.intNorm R S : (a : S) → R) r : R) ((Algebra.intNorm R S : (a : S) → R) x : R)
Tactic: obtain ⟨x, hx', rfl⟩ := (Set.mem_image _ _ _).mp hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst_9 : CommRing Rₘ
inst_10 : Algebra R Rₘ
inst_11 : CommRing Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra Rₘ Sₘ
inst_14 : Algebra R Sₘ
inst_15 : IsScalarTower R Rₘ Sₘ
inst_16 : IsScalarTower R S Sₘ
inst_17 : IsLocalization M Rₘ
inst_18 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_19 : IsIntegrallyClosed Rₘ
inst_20 : IsDomain Rₘ
inst_21 : IsDomain Sₘ
inst_22 : IsTorsionFree Rₘ Sₘ
inst_23 : Module.Finite Rₘ Sₘ
inst_24 : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map (M := Algebra.algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) ⋯
algInst : Algebra Rₘ K := f.toAlgebra
algInst_1 : Algebra Sₘ L := g.toAlgebra
algInst_2 : Algebra Rₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
scalarTowerInst : IsScalarTower Rₘ K L := ⋯
⊢ Eq (α := R →+* K) (algebraMap R K)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ K) (algebraMap R Rₘ))
have rw : Eq (α := R →+* K) (algebraMap R K) (f.comp (algebraMap R Rₘ))
Tactic: rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst_9 : CommRing Rₘ
inst_10 : Algebra R Rₘ
inst_11 : CommRing Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra Rₘ Sₘ
inst_14 : Algebra R Sₘ
inst_15 : IsScalarTower R Rₘ Sₘ
inst_16 : IsScalarTower R S Sₘ
inst_17 : IsLocalization M Rₘ
inst_18 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_19 : IsIntegrallyClosed Rₘ
inst_20 : IsDomain Rₘ
inst_21 : IsDomain Sₘ
inst_22 : IsTorsionFree Rₘ Sₘ
inst_23 : Module.Finite Rₘ Sₘ
inst_24 : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map (M := Algebra.algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) ⋯
algInst : Algebra Rₘ K := f.toAlgebra
algInst_1 : Algebra Sₘ L := g.toAlgebra
algInst_2 : Algebra Rₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
scalarTowerInst : IsScalarTower Rₘ K L := ⋯
rw : Eq (α := R →+* K) (algebraMap R K) (f.comp (algebraMap R Rₘ))
⊢ Eq (α := R →+* K) (algebraMap R K)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ K) (algebraMap R Rₘ))
have rw₁ : Eq (α := R →+* K) (algebraMap R K) (RingHom.comp (algebraMap R K) (RingHom.id R))
Tactic: rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst_9 : CommRing Rₘ
inst_10 : Algebra R Rₘ
inst_11 : CommRing Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra Rₘ Sₘ
inst_14 : Algebra R Sₘ
inst_15 : IsScalarTower R Rₘ Sₘ
inst_16 : IsScalarTower R S Sₘ
inst_17 : IsLocalization M Rₘ
inst_18 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_19 : IsIntegrallyClosed Rₘ
inst_20 : IsDomain Rₘ
inst_21 : IsDomain Sₘ
inst_22 : IsTorsionFree Rₘ Sₘ
inst_23 : Module.Finite Rₘ Sₘ
inst_24 : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map (M := Algebra.algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) ⋯
algInst : Algebra Rₘ K := f.toAlgebra
algInst_1 : Algebra Sₘ L := g.toAlgebra
algInst_2 : Algebra Rₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
scalarTowerInst : IsScalarTower Rₘ K L := ⋯
rw : Eq (α := R →+* K) (algebraMap R K) (f.comp (algebraMap R Rₘ))
rw₁ : Eq (α := R →+* K) (algebraMap R K) (RingHom.comp (algebraMap R K) (RingHom.id R))
⊢ Eq (α := R →+* K) (algebraMap R K)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ K) (algebraMap R Rₘ))
have rw₂ : Eq (α := R →+* K) (algebraMap R K) (algebraMap R K)
Tactic: rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst_9 : CommRing Rₘ
inst_10 : Algebra R Rₘ
inst_11 : CommRing Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra Rₘ Sₘ
inst_14 : Algebra R Sₘ
inst_15 : IsScalarTower R Rₘ Sₘ
inst_16 : IsScalarTower R S Sₘ
inst_17 : IsLocalization M Rₘ
inst_18 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_19 : IsIntegrallyClosed Rₘ
inst_20 : IsDomain Rₘ
inst_21 : IsDomain Sₘ
inst_22 : IsTorsionFree Rₘ Sₘ
inst_23 : Module.Finite Rₘ Sₘ
inst_24 : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map (M := Algebra.algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) ⋯
algInst : Algebra Rₘ K := f.toAlgebra
algInst_1 : Algebra Sₘ L := g.toAlgebra
algInst_2 : Algebra Rₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
scalarTowerInst : IsScalarTower Rₘ K L := ⋯
⊢ Eq (α := Ideal Rₘ) (spanNorm.{u_4, u_5} Rₘ (S := Sₘ) (map (F := S →+* Sₘ) (algebraMap S Sₘ) I))
    (map (F := R →+* Rₘ) (algebraMap R Rₘ) (spanNorm R I))
have this : IsScalarTower R Rₘ K
Tactic: have : IsScalarTower R Rₘ K := IsScalarTower.of_algebraMap_eq'
    (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq])
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst_9 : CommRing Rₘ
inst_10 : Algebra R Rₘ
inst_11 : CommRing Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra Rₘ Sₘ
inst_14 : Algebra R Sₘ
inst_15 : IsScalarTower R Rₘ Sₘ
inst_16 : IsScalarTower R S Sₘ
inst_17 : IsLocalization M Rₘ
inst_18 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_19 : IsIntegrallyClosed Rₘ
inst_20 : IsDomain Rₘ
inst_21 : IsDomain Sₘ
inst_22 : IsTorsionFree Rₘ Sₘ
inst_23 : Module.Finite Rₘ Sₘ
inst_24 : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map (M := Algebra.algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) ⋯
algInst : Algebra Rₘ K := f.toAlgebra
algInst_1 : Algebra Sₘ L := g.toAlgebra
algInst_2 : Algebra Rₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
scalarTowerInst : IsScalarTower Rₘ K L := ⋯
this : IsScalarTower R Rₘ K
h : IsFractionRing Rₘ K := ⋯
⊢ Eq (α := S →+* L) (algebraMap S L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₘ L) (algebraMap S Sₘ))
have rw : Eq (α := S →+* L) (algebraMap S L) (g.comp (algebraMap S Sₘ))
Tactic: rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq]