awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : Eq (α := Ideal R) (spanNorm R I) ⊥
⊢ spanNorm R (I * J) ≤ HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)
have inl : ⊥ ≤ HMul.hMul (α := Ideal R) ⊥ (spanNorm R J)
Tactic: rw [hI, spanNorm_eq_bot_iff.mp hI, bot_mul, spanNorm_bot]
-- 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
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : Eq (α := Ideal R) (spanNorm R I) ⊤
⊢ spanNorm R (I * J) ≤ HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)
have inr : LE.le (α := Ideal R) (spanNorm R (I * J)) (spanNorm R J)
Tactic: rw [hI, Ideal.top_mul]
-- 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
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : Eq (α := Ideal R) (spanNorm R I) ⊤
⊢ LE.le (α := Ideal R) (spanNorm R (I * J)) (spanNorm R J)
have inr : ∀ (hJ : Eq (α := Ideal R) (spanNorm R J) ⊥), LE.le (α := Ideal R) (spanNorm R (I * J)) (spanNorm R J)
Tactic: rcases eq_bot_or_top (spanNorm R J) with hJ | hJ
-- 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
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : Eq (α := Ideal R) (spanNorm R I) ⊤
inr : ∀ (hJ : Eq (α := Ideal R) (spanNorm R J) ⊥), LE.le (α := Ideal R) (spanNorm R (I * J)) (spanNorm R J)
⊢ LE.le (α := Ideal R) (spanNorm R (I * J)) (spanNorm R J)
have inr₁ : ∀ (hJ : Eq (α := Ideal R) (spanNorm R J) ⊤), LE.le (α := Ideal R) (spanNorm R (I * J)) (spanNorm R J)
Tactic: rcases eq_bot_or_top (spanNorm R J) with hJ | hJ
-- 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
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : Eq (α := Ideal R) (spanNorm R I) ⊤
hJ : Eq (α := Ideal R) (spanNorm R J) ⊥
⊢ LE.le (α := Ideal R) (spanNorm R (I * J)) (spanNorm R J)
have inr : LE.le (α := Ideal R) (spanNorm R (I * J)) ⊥
Tactic: rw [hJ, spanNorm_eq_bot_iff.mp hJ, mul_bot, spanNorm_bot]
-- 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
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : Eq (α := Ideal R) (spanNorm R I) ⊤
hJ : Eq (α := Ideal R) (spanNorm R J) ⊥
inr : LE.le (α := Ideal R) (spanNorm R (I * J)) ⊥
⊢ LE.le (α := Ideal R) (spanNorm R (I * J)) (spanNorm R J)
have inr₁ : LE.le (α := Ideal R) (spanNorm R (I * ⊥)) ⊥
Tactic: rw [hJ, spanNorm_eq_bot_iff.mp hJ, mul_bot, spanNorm_bot]
-- 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
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : Eq (α := Ideal R) (spanNorm R I) ⊤
hJ : Eq (α := Ideal R) (spanNorm R J) ⊥
inr : LE.le (α := Ideal R) (spanNorm R (I * J)) ⊥
inr₁ : LE.le (α := Ideal R) (spanNorm R (I * ⊥)) ⊥
⊢ LE.le (α := Ideal R) (spanNorm R (I * J)) (spanNorm R J)
have inr₂ : LE.le (α := Ideal R) (spanNorm.{u_1, u_3} R (S := S) ⊥) ⊥
Tactic: rw [hJ, spanNorm_eq_bot_iff.mp hJ, mul_bot, spanNorm_bot]
-- 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
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : Eq (α := Ideal R) (spanNorm R I) ⊤
hJ : Eq (α := Ideal R) (spanNorm R J) ⊥
inr : LE.le (α := Ideal R) (spanNorm R (I * J)) ⊥
inr₁ : LE.le (α := Ideal R) (spanNorm R (I * ⊥)) ⊥
inr₂ : LE.le (α := Ideal R) (spanNorm.{u_1, u_3} R (S := S) ⊥) ⊥
⊢ LE.le (α := Ideal R) (spanNorm R (I * J)) (spanNorm R J)
have inr₃ : LE.le.{u_1} (α := Ideal R) ⊥ ⊥
Tactic: rw [hJ, spanNorm_eq_bot_iff.mp hJ, mul_bot, spanNorm_bot]
-- 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
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : Eq (α := Ideal R) (spanNorm R I) ⊤
hJ : Eq (α := Ideal R) (spanNorm R J) ⊤
⊢ LE.le (α := Ideal R) (spanNorm R (I * J)) (spanNorm R J)
have inr : LE.le (α := Ideal R) (spanNorm R (I * J)) ⊤
Tactic: rw [hJ]
-- 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
x x_1 : R
h : Membership.mem (γ := Set R) ((⇑(Algebra.intNorm R S) : (a : S) → R) '' (↑I : Set S)) x_1
⊢ Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) I) x_1
have mem : ∀ (x : S) (hx : x ∈ (↑I : Set S)),
  Membership.mem (α := R) (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) I)
    ((Algebra.intNorm R S : (a : S) → R) x : R)
Tactic: obtain ⟨x, hx, rfl⟩ := h
Cleared hypotheses: x_1, h
-- 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
x : R
hx : Membership.mem (γ := Submodule R R) (Submodule.span R ((⇑(Algebra.intNorm R S) : (a : S) → R) '' (↑I : Set S))) x
⊢ Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) I) x
have mem : ∀ (x : R) (h : Membership.mem (γ := Set R) ((⇑(Algebra.intNorm R S) : (a : S) → R) '' (↑I : Set S)) x),
  Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) I) x
Tactic: induction hx using Submodule.span_induction with
  | mem _ h =>
      obtain ⟨x, hx, rfl⟩ := h
      exact mem_comap.mpr <| mem_of_dvd _ (Algebra.dvd_algebraMap_intNorm_self _ _ x) hx
  | zero => simp
  | add _ _ _ _ hx hy => exact Submodule.add_mem _ hx hy
  | smul _ _ _ hx => exact Submodule.smul_mem _ _ hx
Cleared hypotheses: 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
x : R
hx : Membership.mem (γ := Submodule R R) (Submodule.span R ((⇑(Algebra.intNorm R S) : (a : S) → R) '' (↑I : Set S))) x
mem :
  ∀ (x : R) (h : Membership.mem (γ := Set R) ((⇑(Algebra.intNorm R S) : (a : S) → R) '' (↑I : Set S)) x),
    Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) I) x
⊢ Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) I) x
have zero : Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) I) 0
Tactic: induction hx using Submodule.span_induction with
  | mem _ h =>
      obtain ⟨x, hx, rfl⟩ := h
      exact mem_comap.mpr <| mem_of_dvd _ (Algebra.dvd_algebraMap_intNorm_self _ _ x) hx
  | zero => simp
  | add _ _ _ _ hx hy => exact Submodule.add_mem _ hx hy
  | smul _ _ _ hx => exact Submodule.smul_mem _ _ hx
Cleared hypotheses: 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
x : R
hx : Membership.mem (γ := Submodule R R) (Submodule.span R ((⇑(Algebra.intNorm R S) : (a : S) → R) '' (↑I : Set S))) x
mem :
  ∀ (x : R) (h : Membership.mem (γ := Set R) ((⇑(Algebra.intNorm R S) : (a : S) → R) '' (↑I : Set S)) x),
    Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) I) x
zero : Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) I) 0
⊢ Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) I) x
have add : ∀ (x y : R),
  Membership.mem (γ := Submodule R R) (Submodule.span R ((⇑(Algebra.intNorm R S) : (a : S) → R) '' (↑I : Set S))) x →
    Membership.mem (γ := Submodule R R) (Submodule.span R ((⇑(Algebra.intNorm R S) : (a : S) → R) '' (↑I : Set S))) y →
      ∀ (hx : Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) I) x)
        (hy : Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) I) y),
        Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) I) (x + y)
Tactic: induction hx using Submodule.span_induction with
  | mem _ h =>
      obtain ⟨x, hx, rfl⟩ := h
      exact mem_comap.mpr <| mem_of_dvd _ (Algebra.dvd_algebraMap_intNorm_self _ _ x) hx
  | zero => simp
  | add _ _ _ _ hx hy => exact Submodule.add_mem _ hx hy
  | smul _ _ _ hx => exact Submodule.smul_mem _ _ hx
Cleared hypotheses: 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
x : R
hx : Membership.mem (γ := Submodule R R) (Submodule.span R ((⇑(Algebra.intNorm R S) : (a : S) → R) '' (↑I : Set S))) x
mem :
  ∀ (x : R) (h : Membership.mem (γ := Set R) ((⇑(Algebra.intNorm R S) : (a : S) → R) '' (↑I : Set S)) x),
    Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) I) x
zero : Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) I) 0
add :
  ∀ (x y : R),
    Membership.mem (γ := Submodule R R) (Submodule.span R ((⇑(Algebra.intNorm R S) : (a : S) → R) '' (↑I : Set S))) x →
      Membership.mem (γ := Submodule R R) (Submodule.span R ((⇑(Algebra.intNorm R S) : (a : S) → R) '' (↑I : Set S)))
          y →
        ∀ (hx : Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) I) x)
          (hy : Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) I) y),
          Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) I) (x + y)
⊢ Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) I) x
have smul : ∀ (a x : R),
  Membership.mem (γ := Submodule R R) (Submodule.span R ((⇑(Algebra.intNorm R S) : (a : S) → R) '' (↑I : Set S))) x →
    ∀ (hx : Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) I) x),
      Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) I) (a • x)
Tactic: induction hx using Submodule.span_induction with
  | mem _ h =>
      obtain ⟨x, hx, rfl⟩ := h
      exact mem_comap.mpr <| mem_of_dvd _ (Algebra.dvd_algebraMap_intNorm_self _ _ x) hx
  | zero => simp
  | add _ _ _ _ hx hy => exact Submodule.add_mem _ hx hy
  | smul _ _ _ hx => exact Submodule.smul_mem _ _ hx
Cleared hypotheses: hx
-- 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
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
I J : Ideal S
⊢ spanNorm R (I * J) = HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)
have inst : Nontrivial R
Tactic: nontriviality R
-- 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 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
I J : Ideal S
inst_11 : Nontrivial R
⊢ spanNorm R (I * J) = HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)
have inl : Subsingleton S → spanNorm R (I * J) = HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)
Tactic: cases subsingleton_or_nontrivial S
-- 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 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
I J : Ideal S
inst_11 : Nontrivial R
inl : Subsingleton S → spanNorm R (I * J) = HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)
⊢ spanNorm R (I * J) = HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)
have inr : Nontrivial S → spanNorm R (I * J) = HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)
Tactic: cases subsingleton_or_nontrivial S
-- 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
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
I J : Ideal S
inst_11 : Nontrivial R
h : Subsingleton S
⊢ spanNorm R (I * J) = HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)
have this : ∀ (I : Ideal S), I = ⊤
Tactic: have : ∀ I : Ideal S, I = ⊤ := fun I ↦ Subsingleton.elim I ⊤
-- 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 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
I J : Ideal S
inst_11 : Nontrivial R
h : Nontrivial S
⊢ spanNorm R (I * J) = HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)
have inr : ∀ (P : Ideal R) (hP : P.IsMaximal),
  Eq (α := Ideal (Localization.AtPrime P))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P))
      (HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)))
Tactic: refine eq_of_localization_maximal (fun P hP ↦ ?_)
-- 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 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
I J : Ideal S
inst_11 : Nontrivial R
h : Nontrivial S
P : Ideal R
hP : P.IsMaximal
⊢ Eq (α := Ideal (Localization.AtPrime P))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P))
      (HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)))
have pos : ∀ (hP0 : P = ⊥),
  Eq (α := Ideal (Localization.AtPrime P))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P))
      (HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)))
Tactic: by_cases hP0 : P = ⊥
-- 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 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
I J : Ideal S
inst_11 : Nontrivial R
h : Nontrivial S
P : Ideal R
hP : P.IsMaximal
pos :
  ∀ (hP0 : P = ⊥),
    Eq (α := Ideal (Localization.AtPrime P))
      (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)))
      (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P))
        (HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)))
⊢ Eq (α := Ideal (Localization.AtPrime P))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P))
      (HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)))
have neg : ∀ (hP0 : ¬P = ⊥),
  Eq (α := Ideal (Localization.AtPrime P))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P))
      (HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)))
Tactic: by_cases hP0 : P = ⊥
-- 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 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
I J : Ideal S
inst_11 : Nontrivial R
h : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : P = ⊥
⊢ Eq (α := Ideal (Localization.AtPrime P))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P))
      (HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)))
have pos : ∀ (hP : IsMaximal.{u_1} (α := R) ⊥),
  Eq (α := Ideal (Localization.AtPrime (R := R) ⊥))
    (map (F := R →+* Localization.AtPrime (R := R) ⊥) (algebraMap R (Localization.AtPrime (R := R) ⊥))
      (spanNorm R (I * J)))
    (map (F := R →+* Localization.AtPrime (R := R) ⊥) (algebraMap R (Localization.AtPrime (R := R) ⊥))
      (HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)))
Tactic: subst hP0
Cleared hypotheses: P, hP, hP0
-- 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 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
I J : Ideal S
inst_11 : Nontrivial R
h : Nontrivial S
hP : IsMaximal.{u_1} (α := R) ⊥
⊢ Eq (α := Ideal (Localization.AtPrime (R := R) ⊥))
    (map (F := R →+* Localization.AtPrime (R := R) ⊥) (algebraMap R (Localization.AtPrime (R := R) ⊥))
      (spanNorm R (I * J)))
    (map (F := R →+* Localization.AtPrime (R := R) ⊥) (algebraMap R (Localization.AtPrime (R := R) ⊥))
      (HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)))
have pos : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
Tactic: rw [spanNorm_mul_of_bot_or_top]
-- 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
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
I J : Ideal S
inst_11 : Nontrivial R
h : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
⊢ Eq (α := Ideal (Localization.AtPrime P))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P))
      (HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)))
have this : NeZero P
Tactic: have : NeZero P := ⟨hP0⟩
-- 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 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
I J : Ideal S
inst_11 : Nontrivial R
h : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
this : NeZero P
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
⊢ Eq (α := Ideal (Localization.AtPrime P))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P))
      (HMul.hMul (α := Ideal R) (spanNorm R I) (spanNorm R J)))
have neg : spanNorm (Localization.AtPrime P)
    (HMul.hMul (α := Ideal (Localization (M := S) P'))
      (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) I)
      (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) J)) =
  HMul.hMul (α := Ideal (Localization.AtPrime P))
    (spanNorm (Localization.AtPrime P) (S := Localization (M := S) P')
      (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) I))
    (spanNorm (Localization.AtPrime P) (S := Localization (M := S) P')
      (map (F := S →+* Localization (M := S) P') (algebraMap S (Localization (M := S) P')) J))
Tactic: simp only [Ideal.map_mul, ← spanIntNorm_localization (R := R) (Sₘ := Localization P')
    _ _ P.primeCompl_le_nonZeroDivisors]