awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
y'_eq_zero : y' = 0
rw : aJ • y = 0
⊢ HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) aJ : K) y = 0
have rw₁ : Eq.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) y' : K) (0 : K)
Tactic: rw [← Algebra.smul_def, ← hy', y'_eq_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
y'_eq_zero : y' = 0
rw : aJ • y = 0
rw₁ : Eq.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) y' : K) (0 : K)
⊢ HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) aJ : K) y = 0
have rw₂ : Eq.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) 0 : K) (0 : K)
Tactic: rw [← Algebra.smul_def, ← hy', y'_eq_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
y'_eq_zero : y' = 0
rw : aJ • y = 0
rw₁ : Eq.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) y' : K) (0 : K)
rw₂ : Eq.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) 0 : K) (0 : K)
⊢ HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) aJ : K) y = 0
have rw₃ : Eq.{u_4 + 1} (α := K) 0 0
Tactic: rw [← Algebra.smul_def, ← hy', y'_eq_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (hypothesis)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
y'_eq_zero : y' = 0
⊢ False
have this : HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) aJ : K) y = 0
Tactic: have : algebraMap R₁ K aJ * y = 0 := by
        rw [← Algebra.smul_def, ← hy', y'_eq_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (hypothesis)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
y'_eq_zero : y' = 0
this : HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) aJ : K) y = 0
⊢ False
have y_zero : y = 0
Tactic: have y_zero :=
        (mul_eq_zero.mp this).resolve_left
          (mt ((injective_iff_map_eq_zero (algebraMap R₁ K)).1 (IsFractionRing.injective _ _) _)
            (mem_nonZeroDivisors_iff_ne_zero.mp haJ))
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
y'_eq_zero : y' = 0
this : HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) aJ : K) y = 0
y_zero : y = 0
⊢ False
have apply : Membership.mem (γ := Submodule R₁ K) 0 y
Tactic: apply notMem_zero
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
b : K
hb : b ∈ I / J
⊢ IsInteger R₁ ((aI * y') • b)
have h₁ : (aI * y') • b = aI • (b * aJ • y)
Tactic: convert! hI _ (hb _ (Submodule.smul_mem _ aJ mem_J)) using 1
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
b : K
hb : b ∈ I / J
⊢ (aI * y') • b = aI • (b * aJ • y)
have h₁ : (aI * y') • b = aI • HMul.hMul (β := K) b ((algebraMap R₁ K : (a : R₁) → K) y' : K)
Tactic: rw [← hy', mul_comm b, ← Algebra.smul_def, mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
b : K
hb : b ∈ I / J
h₁ : (aI * y') • b = aI • HMul.hMul (β := K) b ((algebraMap R₁ K : (a : R₁) → K) y' : K)
⊢ (aI * y') • b = aI • (b * aJ • y)
have h₂ : (aI * y') • b = aI • HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) y' : K) b
Tactic: rw [← hy', mul_comm b, ← Algebra.smul_def, mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
b : K
hb : b ∈ I / J
h₁ : (aI * y') • b = aI • HMul.hMul (β := K) b ((algebraMap R₁ K : (a : R₁) → K) y' : K)
h₂ : (aI * y') • b = aI • HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) y' : K) b
⊢ (aI * y') • b = aI • (b * aJ • y)
have h₃ : (aI * y') • b = aI • y' • b
Tactic: rw [← hy', mul_comm b, ← Algebra.smul_def, mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
b : K
hb : b ∈ I / J
h₁ : (aI * y') • b = aI • HMul.hMul (β := K) b ((algebraMap R₁ K : (a : R₁) → K) y' : K)
h₂ : (aI * y') • b = aI • HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) y' : K) b
h₃ : (aI * y') • b = aI • y' • b
⊢ (aI * y') • b = aI • (b * aJ • y)
have h₄ : aI • y' • b = aI • y' • b
Tactic: rw [← hy', mul_comm b, ← Algebra.smul_def, mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : J ≠ 0
x : K
⊢ x ∈ I / J ↔ ∀ y ∈ J, x * y ∈ I
have rw : x ∈ Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) ((↑I : Submodule R₁ K) / (↑J : Submodule R₁ K)) sorry ↔
  ∀ y ∈ J, x * y ∈ I
Tactic: rw [div_of_ne_zero h]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
⊢ I * (1 / I) ≤ 1
have pos : ∀ (hI : I = 0), I * (1 / I) ≤ 1
Tactic: by_cases hI : I = 0
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
pos : ∀ (hI : I = 0), I * (1 / I) ≤ 1
⊢ I * (1 / I) ≤ 1
have neg : ∀ (hI : ¬I = 0), I * (1 / I) ≤ 1
Tactic: by_cases hI : I = 0
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : I = 0
⊢ I * (1 / I) ≤ 1
have pos : LE.le.{u_4} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 0 1
Tactic: rw [hI, div_zero, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : ¬I = 0
⊢ I * (1 / I) ≤ 1
have neg : (↑I : Submodule R₁ K) * (1 / (↑I : Submodule R₁ K)) ≤ 1
Tactic: rw [← coe_le_coe, coe_mul, coe_div hI, coe_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : I ≤ 1
⊢ I ≤ I * (1 / I)
have pos : ∀ (hI_nz : I = 0), I ≤ I * (1 / I)
Tactic: by_cases hI_nz : I = 0
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : I ≤ 1
pos : ∀ (hI_nz : I = 0), I ≤ I * (1 / I)
⊢ I ≤ I * (1 / I)
have neg : ∀ (hI_nz : ¬I = 0), I ≤ I * (1 / I)
Tactic: by_cases hI_nz : I = 0
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : I ≤ 1
hI_nz : I = 0
⊢ I ≤ I * (1 / I)
have pos : 0 ≤ 0 * (1 / 0)
Tactic: rw [hI_nz, div_zero, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : I ≤ 1
hI_nz : I = 0
pos : 0 ≤ 0 * (1 / 0)
⊢ I ≤ I * (1 / I)
have pos₁ : 0 ≤ HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 0 0
Tactic: rw [hI_nz, div_zero, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : I ≤ 1
hI_nz : I = 0
pos : 0 ≤ 0 * (1 / 0)
pos₁ : 0 ≤ HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 0 0
⊢ I ≤ I * (1 / I)
have pos₂ : LE.le.{u_4} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 0 0
Tactic: rw [hI_nz, div_zero, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : I ≤ 1
hI_nz : ¬I = 0
⊢ I ≤ I * (1 / I)
have neg : (↑I : Submodule R₁ K) ≤ (↑I : Submodule R₁ K) * (1 / (↑I : Submodule R₁ K))
Tactic: rw [← coe_le_coe, coe_mul, coe_div hI_nz, coe_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (hypothesis)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : I ≤ 1
hI_nz : ¬I = 0
⊢ (↑I : Submodule R₁ K) ≤ (↑I : Submodule R₁ K) * (1 / (↑I : Submodule R₁ K))
have hI₁ : (↑I : Submodule R₁ K) ≤ 1
Tactic: rw [← coe_le_coe, coe_one] at hI
Cleared hypotheses: hI, hI_nz
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I J J' : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hJ' : J' ≠ 0
⊢ I ≤ J / J' ↔ I * J' ≤ J
have rw : I ≤ Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) ((↑J : Submodule R₁ K) / (↑J' : Submodule R₁ K)) sorry ↔
  (↑I : Submodule R₁ K) * (↑J' : Submodule R₁ K) ≤ (↑J : Submodule R₁ K)
Tactic: rw [div_of_ne_zero hJ', ← coe_le_coe (I := I * J') (J := J), coe_mul]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
⊢ I / 1 = I
have rw : Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) ((↑I : Submodule R₁ K) / (↑1 : Submodule R₁ K)) sorry = I
Tactic: rw [div_of_ne_zero (one_ne_zero' (FractionalIdeal R₁⁰ K))]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
⊢ Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) ((↑I : Submodule R₁ K) / (↑1 : Submodule R₁ K)) ⋯ = I
have a : ∀ (x : K),
  x ∈
      Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) ((↑I : Submodule R₁ K) / (↑1 : Submodule R₁ K))
        sorry ↔
    x ∈ I
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
x : K
⊢ x ∈
      Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) ((↑I : Submodule R₁ K) / (↑1 : Submodule R₁ K))
        ⋯ ↔
    x ∈ I
have a : x ∈ Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) ((↑I : Submodule R₁ K) / (↑1 : Submodule R₁ K)) sorry →
  x ∈ I
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
x : K
a :
  x ∈
      Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) ((↑I : Submodule R₁ K) / (↑1 : Submodule R₁ K))
        ⋯ →
    x ∈ I
⊢ x ∈
      Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) ((↑I : Submodule R₁ K) / (↑1 : Submodule R₁ K))
        ⋯ ↔
    x ∈ I
have a₁ : x ∈ I →
  x ∈ Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) ((↑I : Submodule R₁ K) / (↑1 : Submodule R₁ K)) sorry
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
x : K
h : x ∈ I
y' : R₁
left : y' ∈ (↑⊤ : Set R₁)
⊢ HMul.hMul (β := K) x ((Algebra.linearMap R₁ K : (a : R₁) → K) y' : K) ∈ (↑I : Submodule R₁ K)
have h₁ : HMul.hMul (β := K) x ((Algebra.linearMap R₁ K : (a : R₁) → K) y' : K) = y' • x
Tactic: convert! Submodule.smul_mem _ y' h using 1
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
x : K
h : x ∈ I
y' : R₁
left : y' ∈ (↑⊤ : Set R₁)
⊢ HMul.hMul (β := K) x ((Algebra.linearMap R₁ K : (a : R₁) → K) y' : K) = y' • x
have h₁ : HMul.hMul (α := K) ((Algebra.linearMap R₁ K : (a : R₁) → K) y' : K) x = y' • x
Tactic: rw [mul_comm, Algebra.linearMap_apply, ← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
x : K
h : x ∈ I
y' : R₁
left : y' ∈ (↑⊤ : Set R₁)
h₁ : HMul.hMul (α := K) ((Algebra.linearMap R₁ K : (a : R₁) → K) y' : K) x = y' • x
⊢ HMul.hMul (β := K) x ((Algebra.linearMap R₁ K : (a : R₁) → K) y' : K) = y' • x
have h₂ : HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) y' : K) x = y' • x
Tactic: rw [mul_comm, Algebra.linearMap_apply, ← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
x : K
h : x ∈ I
y' : R₁
left : y' ∈ (↑⊤ : Set R₁)
h₁ : HMul.hMul (α := K) ((Algebra.linearMap R₁ K : (a : R₁) → K) y' : K) x = y' • x
h₂ : HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) y' : K) x = y' • x
⊢ HMul.hMul (β := K) x ((Algebra.linearMap R₁ K : (a : R₁) → K) y' : K) = y' • x
have h₃ : y' • x = y' • x
Tactic: rw [mul_comm, Algebra.linearMap_apply, ← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (hypothesis)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
⊢ J = 1 / I
have hI : I ≠ 0
Tactic: have hI : I ≠ 0 := ne_zero_of_mul_eq_one I J h
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ J = 1 / I
have suffices : I * (1 / I) = 1
Tactic: suffices h' : I * (1 / I) = 1 from
    congr_arg Units.inv <| @Units.ext _ _ (Units.mkOfMulEqOne _ _ h) (Units.mkOfMulEqOne _ _ h') rfl
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ I * (1 / I) = 1
have a : I * (1 / I) ≤ 1
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
hI : I ≠ 0
a : I * (1 / I) ≤ 1
⊢ I * (1 / I) = 1
have a₁ : 1 ≤ I * (1 / I)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ I * (1 / I) ≤ 1
have apply : ∀ i ∈ I, ∀ j ∈ 1 / I, Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (i * j)
Tactic: apply mul_le.mpr _
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
hI : I ≠ 0
x : K
hx : x ∈ I
y : K
hy : y ∈ 1 / I
⊢ Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (x * y)
have rw : Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (y * x)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ 1 ≤ I * (1 / I)
have a : I * J ≤ I * (I * J / I)
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ I * J ≤ I * (I * J / I)
have a : J ≤ I * J / I
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ J ≤ I * J / I
have apply : ∀ x ∈ J, ∀ y ∈ I, x * y ∈ I * J
Tactic: apply (le_div_iff_of_ne_zero hI).mpr _
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
hI : I ≠ 0
y : K
hy : y ∈ J
x : K
hx : x ∈ I
⊢ y * x ∈ I * J
have rw : y * x ∈ J * I
Tactic: rw [mul_comm]