-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
lemma den_mem_inv {I : FractionalIdeal R₁⁰ K} (hI : I ≠ ⊥) :
    (algebraMap R₁ K) (I.den : R₁) ∈ I⁻¹

Proof state:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
hI : I ≠ ⊥
⊢ (algebraMap R₁ K) ↑I.den ∈ I⁻¹

Tactic:
rw [mem_inv_iff hI]

Result:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
hI : I ≠ ⊥
⊢ ∀ y ∈ I, (algebraMap R₁ K) ↑I.den * y ∈ 1

Proof state:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
hI : I ≠ ⊥
i : K
hi : i ∈ I
⊢ Submodule.map (Algebra.linearMap R₁ K) I.num ≤ 1

Tactic:
apply le_trans <| map_mono (show I.num ≤ 1 by simp only [Ideal.one_eq_top, le_top, bot_eq_zero])

Result:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
hI : I ≠ ⊥
i : K
hi : i ∈ I
⊢ Submodule.map (Algebra.linearMap R₁ K) 1 ≤ 1

Proof state:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
hI : I ≠ ⊥
i : K
hi : i ∈ I
⊢ ↑I.den • i ∈ 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

Result:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
hI : I ≠ ⊥
i : K
hi : i ∈ I
⊢ Submodule.map (Algebra.linearMap R₁ K) I.num ≤ 1

Proof state:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
hI : I ≠ ⊥
i : K
hi : i ∈ I
⊢ Submodule.map (Algebra.linearMap R₁ K) 1 ≤ 1

Tactic:
rw [Ideal.one_eq_top, Submodule.map_top, one_eq_range]

Result:
no goals

Proof state:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
hI : I ≠ ⊥
i : K
hi : i ∈ I
⊢ I.num ≤ 1

Tactic:
simp only [Ideal.one_eq_top, le_top, bot_eq_zero]

Result:
no goals

Proof state:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
hI : I ≠ ⊥
i : K
hi : i ∈ I
⊢ (algebraMap R₁ K) ↑I.den * i ∈ 1

Tactic:
rw [← Algebra.smul_def (I.den : R₁) i, ← mem_coe, coe_one]

Result:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
hI : I ≠ ⊥
i : K
hi : i ∈ I
⊢ ↑I.den • i ∈ 1

Proof state:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
hI : I ≠ ⊥
⊢ ∀ y ∈ I, (algebraMap R₁ K) ↑I.den * y ∈ 1

Tactic:
intro i hi

Result:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
hI : I ≠ ⊥
i : K
hi : i ∈ I
⊢ (algebraMap R₁ K) ↑I.den * i ∈ 1