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
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
pos₃ : ∀ (h : J = 0) (hI : I = 0), I = J
⊢ I = J
have pos₄ : ∀ (h : 0 = J) (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
pos₃ : ∀ (h : J = 0) (hI : I = 0), I = J
pos₄ : ∀ (h : 0 = J) (hI : I = 0), I = J
⊢ I = J
have pos₅ : ∀ (h : I = J) (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
⊢ I = J
have pos : ∀ (hJ : J = 0), I = J
Tactic: by_cases hJ : J = 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
pos : ∀ (hJ : J = 0), I = J
⊢ I = J
have neg : ∀ (hJ : ¬J = 0), I = J
Tactic: by_cases hJ : J = 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
hJ : J = 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) I :
        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))
  (hI : ¬I = 0) (hJ : J = 0), I = J
Tactic: rwa [hJ, map_zero, extendedHom_eq_zero_iff L B, ← hJ] at h
Cleared hypotheses: h, hI, hJ
-- 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
hJ : J = 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) I :
          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))
    (hI : ¬I = 0) (hJ : J = 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) I :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (0 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L))
  (hI : ¬I = 0) (hJ : J = 0), I = J
Tactic: rwa [hJ, map_zero, extendedHom_eq_zero_iff L B, ← hJ] at h
Cleared hypotheses: h, hI, hJ
-- 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
hJ : J = 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) I :
          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))
    (hI : ¬I = 0) (hJ : J = 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) I :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        (0 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L))
    (hI : ¬I = 0) (hJ : J = 0), I = J
⊢ I = J
have pos₂ : ∀ (h : I = 0) (hI : ¬I = 0) (hJ : J = 0), I = J
Tactic: rwa [hJ, map_zero, extendedHom_eq_zero_iff L B, ← hJ] at h
Cleared hypotheses: h, hI, hJ
-- 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
hJ : J = 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) I :
          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))
    (hI : ¬I = 0) (hJ : J = 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) I :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        (0 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L))
    (hI : ¬I = 0) (hJ : J = 0), I = J
pos₂ : ∀ (h : I = 0) (hI : ¬I = 0) (hJ : J = 0), I = J
⊢ I = J
have pos₃ : ∀ (h : I = J) (hI : ¬I = 0) (hJ : J = 0), I = J
Tactic: rwa [hJ, map_zero, extendedHom_eq_zero_iff L B, ← hJ] at h
Cleared hypotheses: h, hI, hJ
-- 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
hJ : ¬J = 0
⊢ I = J
have neg : ∀
  (h :
    HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) (β := 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) =
      1)
  (hI : ¬I = 0) (hJ : ¬J = 0), I = J
Tactic: rwa [← mul_inv_eq_one₀ ((extendedHom_eq_zero_iff _ _).not.mpr hJ), ← map_inv₀, ← map_mul,
    extendedHom_eq_one_iff _ _ (mul_ne_zero hI (inv_ne_zero hJ)), mul_inv_eq_one₀ hJ] at h
Cleared hypotheses: h, hI, hJ
-- 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
hJ : ¬J = 0
neg :
  ∀
    (h :
      HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) (β := 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) =
        1)
    (hI : ¬I = 0) (hJ : ¬J = 0), I = J
⊢ I = J
have neg₁ : ∀
  (h :
    HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) (β := 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) =
      1)
  (hI : ¬I = 0) (hJ : ¬J = 0), I = J
Tactic: rwa [← mul_inv_eq_one₀ ((extendedHom_eq_zero_iff _ _).not.mpr hJ), ← map_inv₀, ← map_mul,
    extendedHom_eq_one_iff _ _ (mul_ne_zero hI (inv_ne_zero hJ)), mul_inv_eq_one₀ hJ] at h
Cleared hypotheses: h, hI, hJ
-- 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
hJ : ¬J = 0
neg :
  ∀
    (h :
      HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) (β := 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) =
        1)
    (hI : ¬I = 0) (hJ : ¬J = 0), I = J
neg₁ :
  ∀
    (h :
      HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) (β := 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) =
        1)
    (hI : ¬I = 0) (hJ : ¬J = 0), I = J
⊢ I = J
have neg₂ : ∀
  (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 * J⁻¹) :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L))
  (hI : ¬I = 0) (hJ : ¬J = 0), I = J
Tactic: rwa [← mul_inv_eq_one₀ ((extendedHom_eq_zero_iff _ _).not.mpr hJ), ← map_inv₀, ← map_mul,
    extendedHom_eq_one_iff _ _ (mul_ne_zero hI (inv_ne_zero hJ)), mul_inv_eq_one₀ hJ] at h
Cleared hypotheses: h, hI, hJ
-- 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
hJ : ¬J = 0
neg :
  ∀
    (h :
      HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) (β := 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) =
        1)
    (hI : ¬I = 0) (hJ : ¬J = 0), I = J
neg₁ :
  ∀
    (h :
      HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) (β := 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) =
        1)
    (hI : ¬I = 0) (hJ : ¬J = 0), I = J
neg₂ :
  ∀
    (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 * J⁻¹) :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L))
    (hI : ¬I = 0) (hJ : ¬J = 0), I = J
⊢ I = J
have neg₃ : ∀ (h : I * J⁻¹ = 1) (hI : ¬I = 0) (hJ : ¬J = 0), I = J
Tactic: rwa [← mul_inv_eq_one₀ ((extendedHom_eq_zero_iff _ _).not.mpr hJ), ← map_inv₀, ← map_mul,
    extendedHom_eq_one_iff _ _ (mul_ne_zero hI (inv_ne_zero hJ)), mul_inv_eq_one₀ hJ] at h
Cleared hypotheses: h, hI, hJ