awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
I : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
hI : I ≠ 0
rw :
  LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I)⁻¹ :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (1⁻¹ : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
    1 ≤ I
rw₁ :
  LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I)⁻¹ :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
    1 ≤ I
⊢ LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
    1 ≤ I
have rw₂ : LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I⁻¹ :
      FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
  1 ≤ I
Tactic: rw [← inv_le_inv_iff ((extendedHom_eq_zero_iff _ _).not.mpr hI) (by simp), inv_one, ← map_inv₀,
    extendedHom_le_one_iff, inv_le_comm hI (by simp), inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
I : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
hI : I ≠ 0
rw :
  LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I)⁻¹ :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (1⁻¹ : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
    1 ≤ I
rw₁ :
  LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I)⁻¹ :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
    1 ≤ I
rw₂ :
  LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I⁻¹ :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
    1 ≤ I
⊢ LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
    1 ≤ I
have rw₃ : I⁻¹ ≤ 1 ↔ 1 ≤ I
Tactic: rw [← inv_le_inv_iff ((extendedHom_eq_zero_iff _ _).not.mpr hI) (by simp), inv_one, ← map_inv₀,
    extendedHom_le_one_iff, inv_le_comm hI (by simp), inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
I : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
hI : I ≠ 0
rw :
  LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I)⁻¹ :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (1⁻¹ : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
    1 ≤ I
rw₁ :
  LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I)⁻¹ :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
    1 ≤ I
rw₂ :
  LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I⁻¹ :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
    1 ≤ I
rw₃ : I⁻¹ ≤ 1 ↔ 1 ≤ I
⊢ LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
    1 ≤ I
have rw₄ : 1⁻¹ ≤ I ↔ 1 ≤ I
Tactic: rw [← inv_le_inv_iff ((extendedHom_eq_zero_iff _ _).not.mpr hI) (by simp), inv_one, ← map_inv₀,
    extendedHom_le_one_iff, inv_le_comm hI (by simp), inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
I : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
hI : I ≠ 0
rw :
  LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I)⁻¹ :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (1⁻¹ : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
    1 ≤ I
rw₁ :
  LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I)⁻¹ :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
    1 ≤ I
rw₂ :
  LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I⁻¹ :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
    1 ≤ I
rw₃ : I⁻¹ ≤ 1 ↔ 1 ≤ I
rw₄ : 1⁻¹ ≤ I ↔ 1 ≤ I
⊢ LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
    1 ≤ I
have rw₅ : 1 ≤ I ↔ 1 ≤ I
Tactic: rw [← inv_le_inv_iff ((extendedHom_eq_zero_iff _ _).not.mpr hI) (by simp), inv_one, ← map_inv₀,
    extendedHom_le_one_iff, inv_le_comm hI (by simp), inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
I : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
hI : I ≠ 0
⊢ Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
    I = 1
have rw : LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ∧
    LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
  I = 1
Tactic: rw [le_antisymm_iff, extendedHom_le_one_iff, one_le_extendedHom_iff _ _ hI, ← le_antisymm_iff]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
I : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
hI : I ≠ 0
rw :
  LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ∧
      LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
    I = 1
⊢ Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
    I = 1
have rw₁ : I ≤ 1 ∧
    LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
  I = 1
Tactic: rw [le_antisymm_iff, extendedHom_le_one_iff, one_le_extendedHom_iff _ _ hI, ← le_antisymm_iff]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
I : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
hI : I ≠ 0
rw :
  LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ∧
      LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
    I = 1
rw₁ :
  I ≤ 1 ∧
      LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
    I = 1
⊢ Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
    I = 1
have rw₂ : I ≤ 1 ∧ 1 ≤ I ↔ I = 1
Tactic: rw [le_antisymm_iff, extendedHom_le_one_iff, one_le_extendedHom_iff _ _ hI, ← le_antisymm_iff]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
I : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
hI : I ≠ 0
rw :
  LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ∧
      LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
    I = 1
rw₁ :
  I ≤ 1 ∧
      LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
    I = 1
rw₂ : I ≤ 1 ∧ 1 ≤ I ↔ I = 1
⊢ Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
    I = 1
have rw₃ : I = 1 ↔ I = 1
Tactic: rw [le_antisymm_iff, extendedHom_le_one_iff, one_le_extendedHom_iff _ _ hI, ← le_antisymm_iff]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
I J : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
h :
  Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) J : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
⊢ I = J
have pos : ∀ (hI : I = 0), I = J
Tactic: by_cases hI : I = 0
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
I J : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
h :
  Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) J : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
pos : ∀ (hI : I = 0), I = J
⊢ I = J
have neg : ∀ (hI : ¬I = 0), I = J
Tactic: by_cases hI : I = 0
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
I J : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
h :
  Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) J : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
hI : I = 0
⊢ I = J
have pos : ∀
  (h :
    Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) 0 :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) J :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L))
  (hI : I = 0), I = J
Tactic: rwa [hI, map_zero, eq_comm, extendedHom_eq_zero_iff L B, eq_comm, ← hI] at h
Cleared hypotheses: h, hI
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
I J : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
h :
  Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) J : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
hI : I = 0
pos :
  ∀
    (h :
      Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) 0 :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) J :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L))
    (hI : I = 0), I = J
⊢ I = J
have pos₁ : ∀
  (h :
    Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) (0 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) J :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L))
  (hI : I = 0), I = J
Tactic: rwa [hI, map_zero, eq_comm, extendedHom_eq_zero_iff L B, eq_comm, ← hI] at h
Cleared hypotheses: h, hI
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
I J : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
h :
  Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) J : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
hI : I = 0
pos :
  ∀
    (h :
      Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) 0 :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) J :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L))
    (hI : I = 0), I = J
pos₁ :
  ∀
    (h :
      Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) (0 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) J :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L))
    (hI : I = 0), I = J
⊢ I = J
have pos₂ : ∀
  (h :
    Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) J :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (0 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L))
  (hI : I = 0), I = J
Tactic: rwa [hI, map_zero, eq_comm, extendedHom_eq_zero_iff L B, eq_comm, ← hI] at h
Cleared hypotheses: h, hI
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
I J : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
h :
  Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) J : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
hI : I = 0
pos :
  ∀
    (h :
      Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) 0 :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) J :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L))
    (hI : I = 0), I = J
pos₁ :
  ∀
    (h :
      Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) (0 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) J :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L))
    (hI : I = 0), I = J
pos₂ :
  ∀
    (h :
      Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) J :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        (0 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L))
    (hI : I = 0), I = J
⊢ I = J
have pos₃ : ∀ (h : J = 0) (hI : I = 0), I = J
Tactic: rwa [hI, map_zero, eq_comm, extendedHom_eq_zero_iff L B, eq_comm, ← hI] at h
Cleared hypotheses: h, hI