awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
hr : ∃ (x_1 : R), (algebraMap R K : (a : R) → K) x_1 = r • x
h :
  ∀ (r' : R) (hr' : (algebraMap R K : (a : R) → K) r' = r • x),
    ∃ (x_1 : S),
      (algebraMap S L : (a : S) → L) x_1 =
        HSMul.hSMul.{u_6, u_8, u_8} (α := S) (β := L) ((f : (a : R) → S) r : S)
          (((↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) : (a : K) → L) x : L)
⊢ ∃ (x_1 : S),
    (algebraMap S L : (a : S) → L) x_1 =
      HSMul.hSMul.{u_6, u_8, u_8} (α := S) (β := L) ((f : (a : R) → S) r : S)
        (((↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) : (a : K) → L) x : L)

Tactic:
obtain ⟨r', hr'⟩ := hr
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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) =
    HSMul.hSMul.{u_6, u_8, u_8} (α := S) (β := L) ((f : (a : R) → S) r : S)
      (((↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) : (a : K) → L) x : L)
⊢ ∃ (x_1 : S),
    (algebraMap S L : (a : S) → L) x_1 =
      HSMul.hSMul.{u_6, u_8, u_8} (α := S) (β := L) ((f : (a : R) → S) r : S)
        (((↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) : (a : K) → L) x : L)

Tactic:
use f r'

Premises used: DFunLike.coe
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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) =
    HSMul.hSMul.{u_6, u_8, u_8} (α := S) (β := L) ((f : (a : R) → S) r : S)
      ((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)
      (((↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) : (a : K) → L) x : L)

Tactic:
simp only [semilinearEquivOfRingEquiv, RingEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe,
    EquivLike.coe_coe, Equiv.invFun_as_coe, LinearMap.coe_mk, AddHom.coe_mk]

Premises used: Equiv.invFun_as_coe, LinearMap.coe_mk, Equiv.toFun_as_coe, RingEquiv.toEquiv_eq_coe, AddHom.coe_mk, IsFractionRing.semilinearEquivOfRingEquiv, EquivLike.coe_coe
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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)
h₅ 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)
⊢ (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)

Tactic:
rw [Algebra.smul_def, ← ringEquivOfRingEquiv_algebraMap f (K := K) (L := L) r,
    ← map_mul, ← Algebra.smul_def, ← hr', ringEquivOfRingEquiv_algebraMap]

Premises used: IsFractionRing.ringEquivOfRingEquiv_algebraMap, map_mul, Algebra.smul_def
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
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)
⊢ (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

Tactic:
simp only [RingEquiv.symm_symm, val_eq_coe, ← Submodule.map_comp, LinearEquiv.comp_coe,
        coe_ext_iff, coe_mk]

Premises used: FractionalIdeal.coe_ext_iff, FractionalIdeal.coe_mk, Submodule.map_comp, LinearEquiv.comp_coe, RingEquiv.symm_symm, FractionalIdeal.val_eq_coe
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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 LinearMap.id (↑I : Submodule R K) = (↑I : Submodule R K)

Tactic:
Submodule.map_id _

Premises used: Submodule.map_id
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
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
⊢ 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:
convert! Submodule.map_id _

Premises used: Submodule.map_id
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
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)
⊢ 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:
ext
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
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:
simp [semilinearEquivOfRingEquiv, IsLocalization.map_map]

Premises used: IsLocalization.map_map, IsFractionRing.semilinearEquivOfRingEquiv
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
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)
⊢ (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

Tactic:
simp only [RingEquiv.symm_symm, val_eq_coe, ← Submodule.map_comp, LinearEquiv.comp_coe,
        coe_ext_iff, coe_mk]

Premises used: FractionalIdeal.coe_ext_iff, FractionalIdeal.coe_mk, Submodule.map_comp, LinearEquiv.comp_coe, RingEquiv.symm_symm, FractionalIdeal.val_eq_coe
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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 LinearMap.id (↑I : Submodule S L) = (↑I : Submodule S L)

Tactic:
Submodule.map_id _

Premises used: Submodule.map_id
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
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
⊢ 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:
convert! Submodule.map_id _

Premises used: Submodule.map_id
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
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)
⊢ 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:
ext
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
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:
simp [semilinearEquivOfRingEquiv, IsLocalization.map_map]

Premises used: IsLocalization.map_map, IsFractionRing.semilinearEquivOfRingEquiv
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
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))
⊢ 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)) ⋯)

Tactic:
simp only [FractionalIdeal.coe_ext_iff, val_eq_coe, coe_mul, coe_mk]

Premises used: FractionalIdeal.coe_ext_iff, FractionalIdeal.coe_mk, FractionalIdeal.coe_mul, FractionalIdeal.val_eq_coe
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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))
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))
⊢ 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

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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 :
  ∀ m ∈ I,
    ∀ n ∈ J,
      HMul.hMul (α := L) (β := L) ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) m : L)
          ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) n : L) ∈
        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))

Tactic:
simp only [map_le_iff_le_comap, Submodule.mul_le, mem_coe, mem_comap,
          semilinearEquivOfRingEquiv_apply, map_mul, mem_map_equiv,
          semilinearEquivOfRingEquiv_symm_apply, LinearEquiv.coe_coe]

Premises used: Submodule.mem_comap, IsFractionRing.semilinearEquivOfRingEquiv_symm_apply, IsFractionRing.semilinearEquivOfRingEquiv_apply, map_mul, Submodule.mul_le, FractionalIdeal.mem_coe, Submodule.map_le_iff_le_comap, Submodule.mem_map_equiv, LinearEquiv.coe_coe