awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_6
inst_1 : CommRing R₁
inst_2 : Algebra R₁ K
inst_3 : IsLocalization.{u_6, u_3} (R := R₁) R₁⁰ K
I : FractionalIdeal.{u_6, u_3} (R := R₁) R₁⁰ K
inst_4 : (↑I : Submodule R₁ K).IsPrincipal
h : I ≠ 0
a : spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))
| I * spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))⁻¹
have a₁ : spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))⁻¹
Tactic: congr; rw [eq_spanSingleton_of_principal I]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_6
inst_1 : CommRing R₁
inst_2 : Algebra R₁ K
inst_3 : IsLocalization.{u_6, u_3} (R := R₁) R₁⁰ K
I : FractionalIdeal.{u_6, u_3} (R := R₁) R₁⁰ K
inst_4 : (↑I : Submodule R₁ K).IsPrincipal
h : I ≠ 0
⊢ I * spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))⁻¹ = 1
have conv_lhs : HMul.hMul (α := FractionalIdeal.{u_6, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K)))
    (spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))⁻¹) =
  1
Tactic: conv_lhs => congr; rw [eq_spanSingleton_of_principal I]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_6
inst_1 : CommRing R₁
inst_2 : Algebra R₁ K
inst_3 : IsLocalization.{u_6, u_3} (R := R₁) R₁⁰ K
I : FractionalIdeal.{u_6, u_3} (R := R₁) R₁⁰ K
inst_4 : (↑I : Submodule R₁ K).IsPrincipal
h : I ≠ 0
⊢ HMul.hMul (α := FractionalIdeal.{u_6, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K)))
      (spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))⁻¹) =
    1
have rw : generator (↑I : Submodule R₁ K) ≠ 0
Tactic: rw [spanSingleton_mul_spanSingleton, mul_inv_cancel₀, spanSingleton_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_6
inst_1 : CommRing R₁
inst_2 : Algebra R₁ K
inst_3 : IsLocalization.{u_6, u_3} (R := R₁) R₁⁰ K
I : FractionalIdeal.{u_6, u_3} (R := R₁) R₁⁰ K
inst_4 : (↑I : Submodule R₁ K).IsPrincipal
h : I ≠ 0
generator_I_eq_zero : generator (↑I : Submodule R₁ K) = 0
⊢ False
have apply : I = 0
Tactic: apply h
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_6
inst_1 : CommRing R₁
inst_2 : Algebra R₁ K
inst_3 : IsLocalization.{u_6, u_3} (R := R₁) R₁⁰ K
I : FractionalIdeal.{u_6, u_3} (R := R₁) R₁⁰ K
inst_4 : (↑I : Submodule R₁ K).IsPrincipal
h : I ≠ 0
generator_I_eq_zero : generator (↑I : Submodule R₁ K) = 0
⊢ I = 0
have rw : Eq (α := FractionalIdeal.{u_6, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))) 0
Tactic: rw [eq_spanSingleton_of_principal I, generator_I_eq_zero, spanSingleton_zero]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_6
inst_1 : CommRing R₁
inst_2 : Algebra R₁ K
inst_3 : IsLocalization.{u_6, u_3} (R := R₁) R₁⁰ K
I : FractionalIdeal.{u_6, u_3} (R := R₁) R₁⁰ K
inst_4 : (↑I : Submodule R₁ K).IsPrincipal
h : I ≠ 0
generator_I_eq_zero : generator (↑I : Submodule R₁ K) = 0
rw : Eq (α := FractionalIdeal.{u_6, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))) 0
⊢ I = 0
have rw₁ : Eq.{u_3 + 1} (α := FractionalIdeal.{u_6, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ 0) 0
Tactic: rw [eq_spanSingleton_of_principal I, generator_I_eq_zero, spanSingleton_zero]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_6
inst_1 : CommRing R₁
inst_2 : Algebra R₁ K
inst_3 : IsLocalization.{u_6, u_3} (R := R₁) R₁⁰ K
I : FractionalIdeal.{u_6, u_3} (R := R₁) R₁⁰ K
inst_4 : (↑I : Submodule R₁ K).IsPrincipal
h : I ≠ 0
generator_I_eq_zero : generator (↑I : Submodule R₁ K) = 0
rw : Eq (α := FractionalIdeal.{u_6, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))) 0
rw₁ : Eq.{u_3 + 1} (α := FractionalIdeal.{u_6, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ 0) 0
⊢ I = 0
have rw₂ : Eq.{u_3 + 1} (α := FractionalIdeal.{u_6, u_3} (R := R₁) R₁⁰ K) 0 0
Tactic: rw [eq_spanSingleton_of_principal I, generator_I_eq_zero, spanSingleton_zero]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
inst_5 : (↑I : Submodule R₁ K).IsPrincipal
⊢ I * I⁻¹ = 1 ↔ generator (↑I : Submodule R₁ K) ≠ 0
have mp : I * I⁻¹ = 1 → generator (↑I : Submodule R₁ K) ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
inst_5 : (↑I : Submodule R₁ K).IsPrincipal
mp : I * I⁻¹ = 1 → generator (↑I : Submodule R₁ K) ≠ 0
⊢ I * I⁻¹ = 1 ↔ generator (↑I : Submodule R₁ K) ≠ 0
have mpr : generator (↑I : Submodule R₁ K) ≠ 0 → I * I⁻¹ = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
inst_5 : (↑I : Submodule R₁ K).IsPrincipal
hI : I * I⁻¹ = 1
hg : generator (↑I : Submodule R₁ K) = 0
⊢ False
have mp : I = 0
Tactic: apply ne_zero_of_mul_eq_one _ _ hI
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
inst_5 : (↑I : Submodule R₁ K).IsPrincipal
hI : I * I⁻¹ = 1
hg : generator (↑I : Submodule R₁ K) = 0
⊢ I = 0
have mp : Eq (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))) 0
Tactic: rw [eq_spanSingleton_of_principal I, hg, spanSingleton_zero]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
inst_5 : (↑I : Submodule R₁ K).IsPrincipal
hI : I * I⁻¹ = 1
hg : generator (↑I : Submodule R₁ K) = 0
mp : Eq (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))) 0
⊢ I = 0
have mp₁ : Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ 0) 0
Tactic: rw [eq_spanSingleton_of_principal I, hg, spanSingleton_zero]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
inst_5 : (↑I : Submodule R₁ K).IsPrincipal
hI : I * I⁻¹ = 1
hg : generator (↑I : Submodule R₁ K) = 0
mp : Eq (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))) 0
mp₁ : Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ 0) 0
⊢ I = 0
have mp₂ : Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 0 0
Tactic: rw [eq_spanSingleton_of_principal I, hg, spanSingleton_zero]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
inst_5 : (↑I : Submodule R₁ K).IsPrincipal
hg : generator (↑I : Submodule R₁ K) ≠ 0
⊢ I * I⁻¹ = 1
have mpr : I ≠ 0
Tactic: apply invertible_of_principal
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
inst_5 : (↑I : Submodule R₁ K).IsPrincipal
hg : generator (↑I : Submodule R₁ K) ≠ 0
⊢ I ≠ 0
have mpr : Ne (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))) 0
Tactic: rw [eq_spanSingleton_of_principal I]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (hypothesis)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
inst_5 : (↑I : Submodule R₁ K).IsPrincipal
hg : generator (↑I : Submodule R₁ K) ≠ 0
hI : Eq (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))) 0
⊢ False
have this : Membership.mem (γ := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K)))
  (generator (↑I : Submodule R₁ K))
Tactic: have := mem_spanSingleton_self R₁⁰ (generator (I : Submodule R₁ K))
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (hypothesis)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
inst_5 : (↑I : Submodule R₁ K).IsPrincipal
hg : generator (↑I : Submodule R₁ K) ≠ 0
hI : Eq (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))) 0
this :
  Membership.mem (γ := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K)))
    (generator (↑I : Submodule R₁ K))
⊢ False
have this₁ : generator (↑I : Submodule R₁ K) = 0
Tactic: rw [hI, mem_zero_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
inst_5 : (↑I : Submodule R₁ K).IsPrincipal
h : I ≠ 0
⊢ (↑I⁻¹ : Submodule R₁ K).IsPrincipal
have rw : ∃ (x : K), I⁻¹ = spanSingleton R₁⁰ x
Tactic: rw [val_eq_coe, isPrincipal_iff]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
inst_5 : (↑I : Submodule R₁ K).IsPrincipal
h : I ≠ 0
⊢ ∃ (x : K), I⁻¹ = spanSingleton R₁⁰ x
have h₁ : I⁻¹ = spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))⁻¹
Tactic: use (generator (I : Submodule R₁ K))⁻¹
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (hypothesis)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
inst_5 : (↑I : Submodule R₁ K).IsPrincipal
h : I ≠ 0
⊢ I⁻¹ = spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))⁻¹
have hI : I * spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))⁻¹ = 1
Tactic: have hI : I * spanSingleton _ (generator (I : Submodule R₁ K))⁻¹ = 1 :=
    mul_generator_self_inv _ I h
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
hI : I ≠ ⊥
⊢ Membership.mem (α := K) I⁻¹ ((algebraMap R₁ K : (a : R₁) → K) (↑I.den : R₁) : K)
have rw : ∀ y ∈ I,
  Membership.mem (γ := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 1
    (HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) (↑I.den : R₁) : K) y)
Tactic: rw [mem_inv_iff hI]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
hI : I ≠ ⊥
i : K
hi : i ∈ I
⊢ Membership.mem (γ := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 1
    (HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) (↑I.den : R₁) : K) i)
have rw : Membership.mem (γ := Submodule R₁ K) 1 ((↑I.den : R₁) • i)
Tactic: rw [← Algebra.smul_def (I.den : R₁) i, ← mem_coe, coe_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
hI : I ≠ ⊥
i : K
hi : i ∈ I
⊢ Membership.mem (γ := Submodule R₁ K) 1 ((↑I.den : R₁) • i)
have suffices : LE.le (α := Submodule R₁ K) (Submodule.map (Algebra.linearMap R₁ K) I.num) 1
Tactic: suffices Submodule.map (Algebra.linearMap R₁ K) I.num ≤ 1 from
    this <| (den_mul_self_eq_num I).symm ▸ smul_mem_pointwise_smul i I.den I.coeToSubmodule hi
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
hI : I ≠ ⊥
i : K
hi : i ∈ I
⊢ LE.le (α := Submodule R₁ K) (Submodule.map (Algebra.linearMap R₁ K) I.num) 1
have apply : LE.le (α := Submodule R₁ K) (Submodule.map (Algebra.linearMap R₁ K) 1) 1
Tactic: apply le_trans <| map_mono (show I.num ≤ 1 by simp only [Ideal.one_eq_top, le_top])
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
hI : I ≠ ⊥
i : K
hi : i ∈ I
⊢ LE.le (α := Submodule R₁ K) (Submodule.map (Algebra.linearMap R₁ K) 1) 1
have rw : LE.le (α := Submodule R₁ K) (Submodule.map (Algebra.linearMap R₁ K) ⊤) 1
Tactic: rw [Ideal.one_eq_top, Submodule.map_top, one_eq_range]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
hI : I ≠ ⊥
i : K
hi : i ∈ I
rw : LE.le (α := Submodule R₁ K) (Submodule.map (Algebra.linearMap R₁ K) ⊤) 1
⊢ LE.le (α := Submodule R₁ K) (Submodule.map (Algebra.linearMap R₁ K) 1) 1
have rw₁ : LE.le (α := Submodule R₁ K) (LinearMap.range (Algebra.linearMap R₁ K)) 1
Tactic: rw [Ideal.one_eq_top, Submodule.map_top, one_eq_range]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
hI : I ≠ ⊥
i : K
hi : i ∈ I
rw : LE.le (α := Submodule R₁ K) (Submodule.map (Algebra.linearMap R₁ K) ⊤) 1
rw₁ : LE.le (α := Submodule R₁ K) (LinearMap.range (Algebra.linearMap R₁ K)) 1
⊢ LE.le (α := Submodule R₁ K) (Submodule.map (Algebra.linearMap R₁ K) 1) 1
have rw₂ : LE.le (α := Submodule R₁ K) (LinearMap.range (Algebra.linearMap R₁ K)) (LinearMap.range (Algebra.linearMap R₁ K))
Tactic: rw [Ideal.one_eq_top, Submodule.map_top, one_eq_range]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
⊢ (↑I.num : FractionalIdeal R₁⁰ K) ≤ I * I⁻¹
have pos : ∀ (hI : I = 0), (↑I.num : FractionalIdeal R₁⁰ K) ≤ I * I⁻¹
Tactic: by_cases hI : I = 0
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
pos : ∀ (hI : I = 0), (↑I.num : FractionalIdeal R₁⁰ K) ≤ I * I⁻¹
⊢ (↑I.num : FractionalIdeal R₁⁰ K) ≤ I * I⁻¹
have neg : ∀ (hI : ¬I = 0), (↑I.num : FractionalIdeal R₁⁰ K) ≤ I * I⁻¹
Tactic: by_cases hI : I = 0
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
hI : I = 0
⊢ (↑I.num : FractionalIdeal R₁⁰ K) ≤ I * I⁻¹
have pos : (↑(num.{u_4, u_3} (S := R₁⁰) (P := K) 0) : FractionalIdeal R₁⁰ K) ≤
  HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 0 0⁻¹
Tactic: rw [hI, num_zero_eq <| FaithfulSMul.algebraMap_injective R₁ K, zero_mul, zero_eq_bot,
      coeIdeal_bot]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
hI : I = 0
pos :
  (↑(num.{u_4, u_3} (S := R₁⁰) (P := K) 0) : FractionalIdeal R₁⁰ K) ≤
    HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 0 0⁻¹
⊢ (↑I.num : FractionalIdeal R₁⁰ K) ≤ I * I⁻¹
have pos₁ : (↑0 : FractionalIdeal R₁⁰ K) ≤ HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 0 0⁻¹
Tactic: rw [hI, num_zero_eq <| FaithfulSMul.algebraMap_injective R₁ K, zero_mul, zero_eq_bot,
      coeIdeal_bot]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
hI : I = 0
pos :
  (↑(num.{u_4, u_3} (S := R₁⁰) (P := K) 0) : FractionalIdeal R₁⁰ K) ≤
    HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 0 0⁻¹
pos₁ : (↑0 : FractionalIdeal R₁⁰ K) ≤ HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 0 0⁻¹
⊢ (↑I.num : FractionalIdeal R₁⁰ K) ≤ I * I⁻¹
have pos₂ : LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (↑0 : FractionalIdeal R₁⁰ K) 0
Tactic: rw [hI, num_zero_eq <| FaithfulSMul.algebraMap_injective R₁ K, zero_mul, zero_eq_bot,
      coeIdeal_bot]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
hI : I = 0
pos :
  (↑(num.{u_4, u_3} (S := R₁⁰) (P := K) 0) : FractionalIdeal R₁⁰ K) ≤
    HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 0 0⁻¹
pos₁ : (↑0 : FractionalIdeal R₁⁰ K) ≤ HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 0 0⁻¹
pos₂ : LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (↑0 : FractionalIdeal R₁⁰ K) 0
⊢ (↑I.num : FractionalIdeal R₁⁰ K) ≤ I * I⁻¹
have pos₃ : LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (↑⊥ : FractionalIdeal R₁⁰ K) 0
Tactic: rw [hI, num_zero_eq <| FaithfulSMul.algebraMap_injective R₁ K, zero_mul, zero_eq_bot,
      coeIdeal_bot]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
hI : I = 0
pos :
  (↑(num.{u_4, u_3} (S := R₁⁰) (P := K) 0) : FractionalIdeal R₁⁰ K) ≤
    HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 0 0⁻¹
pos₁ : (↑0 : FractionalIdeal R₁⁰ K) ≤ HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 0 0⁻¹
pos₂ : LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (↑0 : FractionalIdeal R₁⁰ K) 0
pos₃ : LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (↑⊥ : FractionalIdeal R₁⁰ K) 0
⊢ (↑I.num : FractionalIdeal R₁⁰ K) ≤ I * I⁻¹
have pos₄ : LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 0 0
Tactic: rw [hI, num_zero_eq <| FaithfulSMul.algebraMap_injective R₁ K, zero_mul, zero_eq_bot,
      coeIdeal_bot]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
hI : ¬I = 0
⊢ (↑I.num : FractionalIdeal R₁⁰ K) ≤ I * I⁻¹
have neg : HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K)
    (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) (↑I.den : R₁)) : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K)
    I ≤
  I⁻¹ * I
Tactic: rw [mul_comm, ← den_mul_self_eq_num']
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Inverse (goal)
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
hI : ¬I = 0
⊢ HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K)
      (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) (↑I.den : R₁)) : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K)
      I ≤
    I⁻¹ * I
have neg : spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) (↑I.den : R₁)) ≤ I⁻¹
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • (↑I : Submodule R K) = Submodule.map (Algebra.linearMap R K) I₀
⊢ HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ) =
    HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑a : R)| : ℚ)
have rw : HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑a : R)| : ℚ) =
  HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
    (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ)
Tactic: rw [div_eq_div_iff]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • (↑I : Submodule R K) = Submodule.map (Algebra.linearMap R K) I₀
rw :
  HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑a : R)| : ℚ) =
    HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ)
⊢ HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ) =
    HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑a : R)| : ℚ)
have hb : Ne (α := ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ) 0
Tactic: rw [div_eq_div_iff]