awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
I : Submodule R K
r : R
hr0 : ¬r = 0
x : K
hx : x ∈ I
r' : R
hr' : (algebraMap R K : (a : R) → K) r' = r • x
⊢ (algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) =
    HSMul.hSMul.{u_6, u_8, u_8} (α := S) (β := L) ((f : (a : R) → S) r : S)
      ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) x : L)
have h : (algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) =
  HMul.hMul (α := L) (β := L) ((algebraMap S L : (a : S) → L) ((f : (a : R) → S) r : S) : L)
    ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) x : L)
Tactic: rw [Algebra.smul_def, ← ringEquivOfRingEquiv_algebraMap f (K := K) (L := L) r,
    ← map_mul, ← Algebra.smul_def, ← hr', ringEquivOfRingEquiv_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
I : Submodule R K
r : R
hr0 : ¬r = 0
x : K
hx : x ∈ I
r' : R
hr' : (algebraMap R K : (a : R) → K) r' = r • x
h :
  (algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) =
    HMul.hMul (α := L) (β := L) ((algebraMap S L : (a : S) → L) ((f : (a : R) → S) r : S) : L)
      ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) x : L)
⊢ (algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) =
    HSMul.hSMul.{u_6, u_8, u_8} (α := S) (β := L) ((f : (a : R) → S) r : S)
      ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) x : L)
have h₁ : (algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) =
  HMul.hMul (α := L) (β := L)
    ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) ((algebraMap R K : (a : R) → K) r : K) : L)
    ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) x : L)
Tactic: rw [Algebra.smul_def, ← ringEquivOfRingEquiv_algebraMap f (K := K) (L := L) r,
    ← map_mul, ← Algebra.smul_def, ← hr', ringEquivOfRingEquiv_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
I : Submodule R K
r : R
hr0 : ¬r = 0
x : K
hx : x ∈ I
r' : R
hr' : (algebraMap R K : (a : R) → K) r' = r • x
h :
  (algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) =
    HMul.hMul (α := L) (β := L) ((algebraMap S L : (a : S) → L) ((f : (a : R) → S) r : S) : L)
      ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) x : L)
h₁ :
  (algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) =
    HMul.hMul (α := L) (β := L)
      ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) ((algebraMap R K : (a : R) → K) r : K) : L)
      ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) x : L)
⊢ (algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) =
    HSMul.hSMul.{u_6, u_8, u_8} (α := S) (β := L) ((f : (a : R) → S) r : S)
      ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) x : L)
have h₂ : Eq.{u_8 + 1} (α := L) ((algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) : L)
  ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) (HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) r : K) x) :
    L)
Tactic: rw [Algebra.smul_def, ← ringEquivOfRingEquiv_algebraMap f (K := K) (L := L) r,
    ← map_mul, ← Algebra.smul_def, ← hr', ringEquivOfRingEquiv_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
I : Submodule R K
r : R
hr0 : ¬r = 0
x : K
hx : x ∈ I
r' : R
hr' : (algebraMap R K : (a : R) → K) r' = r • x
h :
  (algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) =
    HMul.hMul (α := L) (β := L) ((algebraMap S L : (a : S) → L) ((f : (a : R) → S) r : S) : L)
      ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) x : L)
h₁ :
  (algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) =
    HMul.hMul (α := L) (β := L)
      ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) ((algebraMap R K : (a : R) → K) r : K) : L)
      ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) x : L)
h₂ :
  Eq.{u_8 + 1} (α := L) ((algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) : L)
    ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L)
        (HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) r : K) x) :
      L)
⊢ (algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) =
    HSMul.hSMul.{u_6, u_8, u_8} (α := S) (β := L) ((f : (a : R) → S) r : S)
      ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) x : L)
have h₃ : Eq.{u_8 + 1} (α := L) ((algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) : L)
  ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) (r • x) : L)
Tactic: rw [Algebra.smul_def, ← ringEquivOfRingEquiv_algebraMap f (K := K) (L := L) r,
    ← map_mul, ← Algebra.smul_def, ← hr', ringEquivOfRingEquiv_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
I : Submodule R K
r : R
hr0 : ¬r = 0
x : K
hx : x ∈ I
r' : R
hr' : (algebraMap R K : (a : R) → K) r' = r • x
h :
  (algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) =
    HMul.hMul (α := L) (β := L) ((algebraMap S L : (a : S) → L) ((f : (a : R) → S) r : S) : L)
      ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) x : L)
h₁ :
  (algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) =
    HMul.hMul (α := L) (β := L)
      ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) ((algebraMap R K : (a : R) → K) r : K) : L)
      ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) x : L)
h₂ :
  Eq.{u_8 + 1} (α := L) ((algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) : L)
    ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L)
        (HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) r : K) x) :
      L)
h₃ :
  Eq.{u_8 + 1} (α := L) ((algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) : L)
    ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) (r • x) : L)
⊢ (algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) =
    HSMul.hSMul.{u_6, u_8, u_8} (α := S) (β := L) ((f : (a : R) → S) r : S)
      ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) x : L)
have h₄ : Eq.{u_8 + 1} (α := L) ((algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) : L)
  ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) ((algebraMap R K : (a : R) → K) r' : K) : L)
Tactic: rw [Algebra.smul_def, ← ringEquivOfRingEquiv_algebraMap f (K := K) (L := L) r,
    ← map_mul, ← Algebra.smul_def, ← hr', ringEquivOfRingEquiv_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
I : Submodule R K
r : R
hr0 : ¬r = 0
x : K
hx : x ∈ I
r' : R
hr' : (algebraMap R K : (a : R) → K) r' = r • x
h :
  (algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) =
    HMul.hMul (α := L) (β := L) ((algebraMap S L : (a : S) → L) ((f : (a : R) → S) r : S) : L)
      ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) x : L)
h₁ :
  (algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) =
    HMul.hMul (α := L) (β := L)
      ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) ((algebraMap R K : (a : R) → K) r : K) : L)
      ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) x : L)
h₂ :
  Eq.{u_8 + 1} (α := L) ((algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) : L)
    ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L)
        (HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) r : K) x) :
      L)
h₃ :
  Eq.{u_8 + 1} (α := L) ((algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) : L)
    ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) (r • x) : L)
h₄ :
  Eq.{u_8 + 1} (α := L) ((algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) : L)
    ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) ((algebraMap R K : (a : R) → K) r' : K) : L)
⊢ (algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) =
    HSMul.hSMul.{u_6, u_8, u_8} (α := S) (β := L) ((f : (a : R) → S) r : S)
      ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) x : L)
have h₅ : Eq.{u_8 + 1} (α := L) ((algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) : L)
  ((algebraMap S L : (a : S) → L) ((f : (a : R) → S) r' : S) : L)
Tactic: rw [Algebra.smul_def, ← ringEquivOfRingEquiv_algebraMap f (K := K) (L := L) r,
    ← map_mul, ← Algebra.smul_def, ← hr', ringEquivOfRingEquiv_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
S_1 : Submonoid R_1
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R_1 P
R₁ : Type u_3
inst_3 : CommRing R₁
K_1 : Type u_4
inst_4 : Field K_1
inst_5 : Algebra R₁ K_1
inst_6 : IsFractionRing R₁ K_1
inst_7 : IsDomain R₁
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst_8 : CommRing R
inst_9 : IsDomain R
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : CommRing K
inst_13 : CommRing L
inst_14 : Algebra R K
inst_15 : Algebra S L
inst_16 : IsFractionRing R K
inst_17 : IsFractionRing S L
f : R ≃+* S
I : FractionalIdeal.{u_5, u_7} (R := R) R⁰ K
⊢ (fun (J : FractionalIdeal.{u_6, u_8} (R := S) S⁰ L) ↦
        (Subtype.mk (p := fun (I : Submodule R K) ↦ IsFractional R⁰ I)
            (Submodule.map (↑(semilinearEquivOfRingEquiv L K f.symm) : L →ₛₗ[(↑f.symm : S →+* R)] K)
              (↑J : Submodule S L))
            ⋯ :
          { I : Submodule R K // IsFractional R⁰ I }))
      ((fun (I : FractionalIdeal.{u_5, u_7} (R := R) R⁰ K) ↦
          (Subtype.mk (p := fun (I : Submodule S L) ↦ IsFractional S⁰ I)
              (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑I : Submodule R K)) ⋯ :
            { I : Submodule S L // IsFractional S⁰ I }))
        I) =
    I
have simp : Submodule.map
    (↑(LinearEquiv.trans (module_M₂ := Algebra.toModule) (semilinearEquivOfRingEquiv K L f)
          (semilinearEquivOfRingEquiv L K f.symm)) :
      K →ₗ[R] K)
    (↑I : Submodule R K) =
  (↑I : Submodule R K)
Tactic: simp only [RingEquiv.symm_symm, val_eq_coe, ← Submodule.map_comp, LinearEquiv.comp_coe,
        coe_ext_iff, coe_mk]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
S_1 : Submonoid R_1
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R_1 P
R₁ : Type u_3
inst_3 : CommRing R₁
K_1 : Type u_4
inst_4 : Field K_1
inst_5 : Algebra R₁ K_1
inst_6 : IsFractionRing R₁ K_1
inst_7 : IsDomain R₁
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst_8 : CommRing R
inst_9 : IsDomain R
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : CommRing K
inst_13 : CommRing L
inst_14 : Algebra R K
inst_15 : Algebra S L
inst_16 : IsFractionRing R K
inst_17 : IsFractionRing S L
f : R ≃+* S
I : FractionalIdeal.{u_5, u_7} (R := R) R⁰ K
⊢ Submodule.map
      (↑(LinearEquiv.trans (module_M₂ := Algebra.toModule) (semilinearEquivOfRingEquiv K L f)
            (semilinearEquivOfRingEquiv L K f.symm)) :
        K →ₗ[R] K)
      (↑I : Submodule R K) =
    (↑I : Submodule R K)
have h : Eq (α := K →ₗ[R] K)
  (↑(LinearEquiv.trans (module_M₂ := Algebra.toModule) (semilinearEquivOfRingEquiv K L f)
        (semilinearEquivOfRingEquiv L K f.symm)) :
    K →ₗ[R] K)
  LinearMap.id
Tactic: convert! Submodule.map_id _
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
S_1 : Submonoid R_1
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R_1 P
R₁ : Type u_3
inst_3 : CommRing R₁
K_1 : Type u_4
inst_4 : Field K_1
inst_5 : Algebra R₁ K_1
inst_6 : IsFractionRing R₁ K_1
inst_7 : IsDomain R₁
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst_8 : CommRing R
inst_9 : IsDomain R
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : CommRing K
inst_13 : CommRing L
inst_14 : Algebra R K
inst_15 : Algebra S L
inst_16 : IsFractionRing R K
inst_17 : IsFractionRing S L
f : R ≃+* S
I : FractionalIdeal.{u_5, u_7} (R := R) R⁰ K
⊢ Eq (α := K →ₗ[R] K)
    (↑(LinearEquiv.trans (module_M₂ := Algebra.toModule) (semilinearEquivOfRingEquiv K L f)
          (semilinearEquivOfRingEquiv L K f.symm)) :
      K →ₗ[R] K)
    LinearMap.id
have h : ∀ (x : K),
  Eq (α := K)
    (((↑(LinearEquiv.trans (module_M₂ := Algebra.toModule) (semilinearEquivOfRingEquiv K L f)
                (semilinearEquivOfRingEquiv L K f.symm)) :
            K →ₗ[R] K) :
          (a : K) → K)
        x :
      K)
    ((LinearMap.id : (a : K) → K) x : K)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
S_1 : Submonoid R_1
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R_1 P
R₁ : Type u_3
inst_3 : CommRing R₁
K_1 : Type u_4
inst_4 : Field K_1
inst_5 : Algebra R₁ K_1
inst_6 : IsFractionRing R₁ K_1
inst_7 : IsDomain R₁
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst_8 : CommRing R
inst_9 : IsDomain R
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : CommRing K
inst_13 : CommRing L
inst_14 : Algebra R K
inst_15 : Algebra S L
inst_16 : IsFractionRing R K
inst_17 : IsFractionRing S L
f : R ≃+* S
I : FractionalIdeal.{u_6, u_8} (R := S) S⁰ L
⊢ (fun (I : FractionalIdeal.{u_5, u_7} (R := R) R⁰ K) ↦
        (Subtype.mk (p := fun (I : Submodule S L) ↦ IsFractional S⁰ I)
            (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑I : Submodule R K)) ⋯ :
          { I : Submodule S L // IsFractional S⁰ I }))
      ((fun (J : FractionalIdeal.{u_6, u_8} (R := S) S⁰ L) ↦
          (Subtype.mk (p := fun (I : Submodule R K) ↦ IsFractional R⁰ I)
              (Submodule.map (↑(semilinearEquivOfRingEquiv L K f.symm) : L →ₛₗ[(↑f.symm : S →+* R)] K)
                (↑J : Submodule S L))
              ⋯ :
            { I : Submodule R K // IsFractional R⁰ I }))
        I) =
    I
have simp : Submodule.map
    (↑(LinearEquiv.trans (module_M₂ := Algebra.toModule) (semilinearEquivOfRingEquiv L K f.symm)
          (semilinearEquivOfRingEquiv K L f)) :
      L →ₗ[S] L)
    (↑I : Submodule S L) =
  (↑I : Submodule S L)
Tactic: simp only [RingEquiv.symm_symm, val_eq_coe, ← Submodule.map_comp, LinearEquiv.comp_coe,
        coe_ext_iff, coe_mk]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
S_1 : Submonoid R_1
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R_1 P
R₁ : Type u_3
inst_3 : CommRing R₁
K_1 : Type u_4
inst_4 : Field K_1
inst_5 : Algebra R₁ K_1
inst_6 : IsFractionRing R₁ K_1
inst_7 : IsDomain R₁
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst_8 : CommRing R
inst_9 : IsDomain R
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : CommRing K
inst_13 : CommRing L
inst_14 : Algebra R K
inst_15 : Algebra S L
inst_16 : IsFractionRing R K
inst_17 : IsFractionRing S L
f : R ≃+* S
I : FractionalIdeal.{u_6, u_8} (R := S) S⁰ L
⊢ Submodule.map
      (↑(LinearEquiv.trans (module_M₂ := Algebra.toModule) (semilinearEquivOfRingEquiv L K f.symm)
            (semilinearEquivOfRingEquiv K L f)) :
        L →ₗ[S] L)
      (↑I : Submodule S L) =
    (↑I : Submodule S L)
have h : Eq (α := L →ₗ[S] L)
  (↑(LinearEquiv.trans (module_M₂ := Algebra.toModule) (semilinearEquivOfRingEquiv L K f.symm)
        (semilinearEquivOfRingEquiv K L f)) :
    L →ₗ[S] L)
  LinearMap.id
Tactic: convert! Submodule.map_id _
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
S_1 : Submonoid R_1
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R_1 P
R₁ : Type u_3
inst_3 : CommRing R₁
K_1 : Type u_4
inst_4 : Field K_1
inst_5 : Algebra R₁ K_1
inst_6 : IsFractionRing R₁ K_1
inst_7 : IsDomain R₁
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst_8 : CommRing R
inst_9 : IsDomain R
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : CommRing K
inst_13 : CommRing L
inst_14 : Algebra R K
inst_15 : Algebra S L
inst_16 : IsFractionRing R K
inst_17 : IsFractionRing S L
f : R ≃+* S
I : FractionalIdeal.{u_6, u_8} (R := S) S⁰ L
⊢ Eq (α := L →ₗ[S] L)
    (↑(LinearEquiv.trans (module_M₂ := Algebra.toModule) (semilinearEquivOfRingEquiv L K f.symm)
          (semilinearEquivOfRingEquiv K L f)) :
      L →ₗ[S] L)
    LinearMap.id
have h : ∀ (x : L),
  Eq (α := L)
    (((↑(LinearEquiv.trans (module_M₂ := Algebra.toModule) (semilinearEquivOfRingEquiv L K f.symm)
                (semilinearEquivOfRingEquiv K L f)) :
            L →ₗ[S] L) :
          (a : L) → L)
        x :
      L)
    ((LinearMap.id : (a : L) → L) x : L)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
S_1 : Submonoid R_1
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R_1 P
R₁ : Type u_3
inst_3 : CommRing R₁
K_1 : Type u_4
inst_4 : Field K_1
inst_5 : Algebra R₁ K_1
inst_6 : IsFractionRing R₁ K_1
inst_7 : IsDomain R₁
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst_8 : CommRing R
inst_9 : IsDomain R
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : CommRing K
inst_13 : CommRing L
inst_14 : Algebra R K
inst_15 : Algebra S L
inst_16 : IsFractionRing R K
inst_17 : IsFractionRing S L
f : R ≃+* S
I J : FractionalIdeal.{u_5, u_7} (R := R) R⁰ K
⊢ Subtype.mk (p := fun (I : Submodule S L) ↦ IsFractional S⁰ I)
      (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑(I * J) : Submodule R K)) ⋯ =
    HMul.hMul (α := FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)
      (Subtype.mk (p := fun (I : Submodule S L) ↦ IsFractional S⁰ I)
        (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑I : Submodule R K)) ⋯)
      (Subtype.mk (p := fun (I : Submodule S L) ↦ IsFractional S⁰ I)
        (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑J : Submodule R K)) ⋯)
have simp : Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L)
    ((↑I : Submodule R K) * (↑J : Submodule R K)) =
  HMul.hMul (α := Submodule S L)
    (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑I : Submodule R K))
    (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑J : Submodule R K))
Tactic: simp only [FractionalIdeal.coe_ext_iff, val_eq_coe, coe_mul, coe_mk]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
S_1 : Submonoid R_1
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R_1 P
R₁ : Type u_3
inst_3 : CommRing R₁
K_1 : Type u_4
inst_4 : Field K_1
inst_5 : Algebra R₁ K_1
inst_6 : IsFractionRing R₁ K_1
inst_7 : IsDomain R₁
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst_8 : CommRing R
inst_9 : IsDomain R
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : CommRing K
inst_13 : CommRing L
inst_14 : Algebra R K
inst_15 : Algebra S L
inst_16 : IsFractionRing R K
inst_17 : IsFractionRing S L
f : R ≃+* S
I J : FractionalIdeal.{u_5, u_7} (R := R) R⁰ K
⊢ Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L)
      ((↑I : Submodule R K) * (↑J : Submodule R K)) =
    HMul.hMul (α := Submodule S L)
      (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑I : Submodule R K))
      (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑J : Submodule R K))
have a : Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L)
    ((↑I : Submodule R K) * (↑J : Submodule R K)) ≤
  HMul.hMul (α := Submodule S L)
    (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑I : Submodule R K))
    (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑J : Submodule R K))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
S_1 : Submonoid R_1
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R_1 P
R₁ : Type u_3
inst_3 : CommRing R₁
K_1 : Type u_4
inst_4 : Field K_1
inst_5 : Algebra R₁ K_1
inst_6 : IsFractionRing R₁ K_1
inst_7 : IsDomain R₁
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst_8 : CommRing R
inst_9 : IsDomain R
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : CommRing K
inst_13 : CommRing L
inst_14 : Algebra R K
inst_15 : Algebra S L
inst_16 : IsFractionRing R K
inst_17 : IsFractionRing S L
f : R ≃+* S
I J : FractionalIdeal.{u_5, u_7} (R := R) R⁰ K
a :
  Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L)
      ((↑I : Submodule R K) * (↑J : Submodule R K)) ≤
    HMul.hMul (α := Submodule S L)
      (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑I : Submodule R K))
      (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑J : Submodule R K))
⊢ Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L)
      ((↑I : Submodule R K) * (↑J : Submodule R K)) =
    HMul.hMul (α := Submodule S L)
      (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑I : Submodule R K))
      (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑J : Submodule R K))
have a₁ : HMul.hMul (α := Submodule S L)
    (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑I : Submodule R K))
    (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑J : Submodule R K)) ≤
  Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L)
    ((↑I : Submodule R K) * (↑J : Submodule R K))
Tactic: apply le_antisymm