awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
x : K
hx : x ≠ 0
rw : Eq (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ (x / x)) 1
rw₁ : Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ 1) 1
rw₂ rw₃ : Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 1 1
⊢ HDiv.hDiv (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ x) (spanSingleton R₁⁰ x) = 1

Tactic:
rw [spanSingleton_div_spanSingleton, div_self hx, spanSingleton_one]

Premises used: FractionalIdeal.spanSingleton_div_spanSingleton, FractionalIdeal.spanSingleton_one, div_self
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
x : R₁
hx : x ≠ 0
rw :
  HDiv.hDiv (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (β := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K)
      (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x) : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K)
      (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x) : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) =
    1
rw₁ rw₂ : Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 1 1
⊢ HDiv.hDiv (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (↑(Ideal.span {x}) : FractionalIdeal R₁⁰ K)
      (↑(Ideal.span {x}) : FractionalIdeal R₁⁰ K) =
    1

Tactic:
rw [coeIdeal_span_singleton,
    spanSingleton_div_self K <|
      (map_ne_zero_iff _ <| FaithfulSMul.algebraMap_injective R₁ K).mpr hx]

Premises used: Iff.mpr, FractionalIdeal.coeIdeal_span_singleton, FaithfulSMul.algebraMap_injective, map_ne_zero_iff, FractionalIdeal.spanSingleton_div_self
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
x : K
hx : x ≠ 0
rw : HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ x) (spanSingleton R₁⁰ x⁻¹) = 1
rw₁ : Eq (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ (x * x⁻¹)) 1
rw₂ : Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ 1) 1
rw₃ rw₄ : Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 1 1
⊢ HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ x) (spanSingleton R₁⁰ x)⁻¹ = 1

Tactic:
rw [spanSingleton_inv, spanSingleton_mul_spanSingleton, mul_inv_cancel₀ hx, spanSingleton_one]

Premises used: mul_inv_cancel₀, FractionalIdeal.spanSingleton_mul_spanSingleton, FractionalIdeal.spanSingleton_one, FractionalIdeal.spanSingleton_inv
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
x : R₁
hx : x ≠ 0
rw :
  HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (β := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K)
      (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x) : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K)
      ((spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x))⁻¹ : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) =
    1
rw₁ rw₂ : Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 1 1
⊢ HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (↑(Ideal.span {x}) : FractionalIdeal R₁⁰ K)
      (↑(Ideal.span {x}) : FractionalIdeal R₁⁰ K)⁻¹ =
    1

Tactic:
rw [coeIdeal_span_singleton,
    spanSingleton_mul_inv K <|
      (map_ne_zero_iff _ <| FaithfulSMul.algebraMap_injective R₁ K).mpr hx]

Premises used: FractionalIdeal.spanSingleton_mul_inv, Iff.mpr, FractionalIdeal.coeIdeal_span_singleton, FaithfulSMul.algebraMap_injective, map_ne_zero_iff
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
x : K
hx : x ≠ 0
rw : HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ x) (spanSingleton R₁⁰ x)⁻¹ = 1
rw₁ rw₂ : Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 1 1
⊢ HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ x)⁻¹ (spanSingleton R₁⁰ x) = 1

Tactic:
rw [mul_comm, spanSingleton_mul_inv K hx]

Premises used: FractionalIdeal.spanSingleton_mul_inv, mul_comm
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
x : R₁
hx : x ≠ 0
rw :
  HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (↑(Ideal.span {x}) : FractionalIdeal R₁⁰ K)
      (↑(Ideal.span {x}) : FractionalIdeal R₁⁰ K)⁻¹ =
    1
rw₁ rw₂ : Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 1 1
⊢ HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (↑(Ideal.span {x}) : FractionalIdeal R₁⁰ K)⁻¹
      (↑(Ideal.span {x}) : FractionalIdeal R₁⁰ K) =
    1

Tactic:
rw [mul_comm, coe_ideal_span_singleton_mul_inv K hx]

Premises used: mul_comm, FractionalIdeal.coe_ideal_span_singleton_mul_inv
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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 : I
a₁ : spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))⁻¹
| I * spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))⁻¹

Tactic:
congr
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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

Tactic:
rw [eq_spanSingleton_of_principal I]

Premises used: FractionalIdeal.eq_spanSingleton_of_principal
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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))
a₁ : spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))⁻¹
| I * spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))⁻¹

Tactic:
congr; rw [eq_spanSingleton_of_principal I]

Premises used: FractionalIdeal.eq_spanSingleton_of_principal
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
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
⊢ I * spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))⁻¹ = 1

Tactic:
conv_lhs => congr; rw [eq_spanSingleton_of_principal I]

Premises used: FractionalIdeal.eq_spanSingleton_of_principal
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
rw : generator (↑I : Submodule R₁ K) ≠ 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

Tactic:
rw [spanSingleton_mul_spanSingleton, mul_inv_cancel₀, spanSingleton_one]

Premises used: mul_inv_cancel₀, FractionalIdeal.spanSingleton_mul_spanSingleton, FractionalIdeal.spanSingleton_one
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
apply : I = 0
⊢ False

Tactic:
apply h
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
rw₂ rw₃ : Eq.{u_3 + 1} (α := FractionalIdeal.{u_6, u_3} (R := R₁) R₁⁰ K) 0 0
⊢ I = 0

Tactic:
rw [eq_spanSingleton_of_principal I, generator_I_eq_zero, spanSingleton_zero]

Premises used: FractionalIdeal.spanSingleton_zero, FractionalIdeal.eq_spanSingleton_of_principal
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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 * I⁻¹ = 1

Tactic:
mul_div_self_cancel_iff.mpr
    ⟨spanSingleton _ (generator (I : Submodule R₁ K))⁻¹, mul_generator_self_inv _ I h⟩

Premises used: Iff.mpr, FractionalIdeal.spanSingleton, FractionalIdeal.mul_generator_self_inv, Submodule.IsPrincipal.generator, FractionalIdeal.coeToSubmodule, Inv.inv, Exists.intro, FractionalIdeal.mul_div_self_cancel_iff
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
mpr : generator (↑I : Submodule R₁ K) ≠ 0 → I * I⁻¹ = 1
⊢ I * I⁻¹ = 1 ↔ generator (↑I : Submodule R₁ K) ≠ 0

Tactic:
constructor
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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 : I = 0
⊢ False

Tactic:
apply ne_zero_of_mul_eq_one _ _ hI

Premises used: FractionalIdeal.ne_zero_of_mul_eq_one
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
mp₂ mp₃ : Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 0 0
⊢ I = 0

Tactic:
rw [eq_spanSingleton_of_principal I, hg, spanSingleton_zero]

Premises used: FractionalIdeal.spanSingleton_zero, FractionalIdeal.eq_spanSingleton_of_principal
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
mpr : I ≠ 0
⊢ I * I⁻¹ = 1

Tactic:
apply invertible_of_principal

Premises used: FractionalIdeal.invertible_of_principal
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
mpr : Ne (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))) 0
⊢ I ≠ 0

Tactic:
rw [eq_spanSingleton_of_principal I]

Premises used: FractionalIdeal.eq_spanSingleton_of_principal
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
⊢ 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))
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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))
⊢ generator (↑I : Submodule R₁ K) = 0

Tactic:
rw [hI, mem_zero_iff] at this

Premises used: FractionalIdeal.mem_zero_iff
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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 : generator (↑I : Submodule R₁ K) = 0
⊢ False

Tactic:
contradiction
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
rw : ∃ (x : K), I⁻¹ = spanSingleton R₁⁰ x
⊢ (↑I⁻¹ : Submodule R₁ K).IsPrincipal

Tactic:
rw [val_eq_coe, isPrincipal_iff]

Premises used: FractionalIdeal.isPrincipal_iff, FractionalIdeal.val_eq_coe
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
h₁ : I⁻¹ = spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))⁻¹
⊢ ∃ (x : K), I⁻¹ = spanSingleton R₁⁰ x

Tactic:
use (generator (I : Submodule R₁ K))⁻¹

Premises used: Submodule.IsPrincipal.generator, FractionalIdeal.coeToSubmodule
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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))⁻¹ = 1

Tactic:
have hI : I * spanSingleton _ (generator (I : Submodule R₁ K))⁻¹ = 1 :=
    mul_generator_self_inv _ I h
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
hI : I * spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))⁻¹ = 1
⊢ I⁻¹ = spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))⁻¹

Tactic:
(right_inverse_eq _ I (spanSingleton _ (generator (I : Submodule R₁ K))⁻¹) hI).symm

Premises used: FractionalIdeal.spanSingleton, FractionalIdeal.right_inverse_eq, Submodule.IsPrincipal.generator, FractionalIdeal.coeToSubmodule, Inv.inv, Eq.symm
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
hI : I * spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))⁻¹ = 1
⊢ I⁻¹ = spanSingleton R₁⁰ (generator (↑I : Submodule R₁ K))⁻¹

Tactic:
exact (right_inverse_eq _ I (spanSingleton _ (generator (I : Submodule R₁ K))⁻¹) hI).symm

Premises used: FractionalIdeal.spanSingleton, FractionalIdeal.right_inverse_eq, Submodule.IsPrincipal.generator, FractionalIdeal.coeToSubmodule, Inv.inv, Eq.symm
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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 ≠ ⊥
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)
⊢ Membership.mem (α := K) I⁻¹ ((algebraMap R₁ K : (a : R₁) → K) (↑I.den : R₁) : K)

Tactic:
rw [mem_inv_iff hI]

Premises used: FractionalIdeal.mem_inv_iff
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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 : Membership.mem (γ := Submodule R₁ K) 1 ((↑I.den : R₁) • 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)

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

Premises used: FractionalIdeal.coe_one, FractionalIdeal.den, FractionalIdeal.mem_coe, Algebra.smul_def, Subtype.val
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
suffices : LE.le (α := Submodule R₁ K) (Submodule.map (Algebra.linearMap R₁ K) I.num) 1
⊢ Membership.mem (γ := Submodule R₁ K) 1 ((↑I.den : R₁) • i)

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
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
⊢ I.num ≤ 1

Tactic:
simp only [Ideal.one_eq_top, le_top]

Premises used: Ideal.one_eq_top, le_top
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
apply : LE.le (α := Submodule R₁ K) (Submodule.map (Algebra.linearMap R₁ K) 1) 1
⊢ LE.le (α := Submodule R₁ K) (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])

Premises used: Submodule.map_mono, le_trans
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
rw₂ rw₃ :
  LE.le (α := Submodule R₁ K) (LinearMap.range (Algebra.linearMap R₁ K)) (LinearMap.range (Algebra.linearMap R₁ K))
⊢ LE.le (α := Submodule R₁ K) (Submodule.map (Algebra.linearMap R₁ K) 1) 1

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

Premises used: Ideal.one_eq_top, Submodule.map_top, Submodule.one_eq_range
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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⁻¹
neg : ∀ (hI : ¬I = 0), (↑I.num : FractionalIdeal R₁⁰ K) ≤ I * I⁻¹
⊢ (↑I.num : FractionalIdeal R₁⁰ K) ≤ I * I⁻¹

Tactic:
by_cases hI : I = 0
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
pos₄ pos₅ : LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 0 0
⊢ (↑I.num : FractionalIdeal R₁⁰ K) ≤ I * I⁻¹

Tactic:
rw [hI, num_zero_eq <| FaithfulSMul.algebraMap_injective R₁ K, zero_mul, zero_eq_bot,
      coeIdeal_bot]

Premises used: MulZeroClass.zero_mul, FractionalIdeal.num_zero_eq, FractionalIdeal.coeIdeal_bot, FaithfulSMul.algebraMap_injective, Submodule.zero_eq_bot
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
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
⊢ (↑I.num : FractionalIdeal R₁⁰ K) ≤ I * I⁻¹

Tactic:
rw [mul_comm, ← den_mul_self_eq_num']

Premises used: mul_comm, FractionalIdeal.den_mul_self_eq_num'
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
neg : spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) (↑I.den : R₁)) ≤ I⁻¹
⊢ 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:
gcongr
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
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
⊢ spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) (↑I.den : R₁)) ≤ I⁻¹

Tactic:
spanSingleton_le_iff_mem.2 (den_mem_inv hI)

Premises used: Iff.mpr, FractionalIdeal.spanSingleton_le_iff_mem, FractionalIdeal.den_mem_inv