awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : L),
    Membership.mem (α := K) I ((RingEquiv.symm (IsFractionRing.ringEquivOfRingEquiv f) : (a : L) → K) m : K) →
      ∀ (n : L),
        Membership.mem (α := K) J ((RingEquiv.symm (IsFractionRing.ringEquivOfRingEquiv f) : (a : L) → K) n : K) →
          HMul.hMul (α := K) (β := K) ((RingEquiv.symm (IsFractionRing.ringEquivOfRingEquiv f) : (a : L) → K) m : K)
              ((RingEquiv.symm (IsFractionRing.ringEquivOfRingEquiv f) : (a : L) → K) n : K) ∈
            (↑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))

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
-- 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
⊢ ∀ 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))

Tactic:
fun m hm n hn ↦ Submodule.mul_mem_mul (mem_map_of_mem hm) (mem_map_of_mem hn)

Premises used: Submodule.mul_mem_mul, Set.Mem, Submodule.mem_map_of_mem
-- 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
⊢ ∀ 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))

Tactic:
exact fun m hm n hn ↦ Submodule.mul_mem_mul (mem_map_of_mem hm) (mem_map_of_mem hn)

Premises used: Submodule.mul_mem_mul, Submodule.mem_map_of_mem
-- 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
⊢ ∀ (m : L),
    Membership.mem (α := K) I ((RingEquiv.symm (IsFractionRing.ringEquivOfRingEquiv f) : (a : L) → K) m : K) →
      ∀ (n : L),
        Membership.mem (α := K) J ((RingEquiv.symm (IsFractionRing.ringEquivOfRingEquiv f) : (a : L) → K) n : K) →
          HMul.hMul (α := K) (β := K) ((RingEquiv.symm (IsFractionRing.ringEquivOfRingEquiv f) : (a : L) → K) m : K)
              ((RingEquiv.symm (IsFractionRing.ringEquivOfRingEquiv f) : (a : L) → K) n : K) ∈
            (↑I : Submodule R K) * (↑J : Submodule R K)

Tactic:
fun m hm n hn ↦ Submodule.mul_mem_mul hm hn

Premises used: Submodule.mul_mem_mul, Set.Mem
-- 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
⊢ ∀ (m : L),
    Membership.mem (α := K) I ((RingEquiv.symm (IsFractionRing.ringEquivOfRingEquiv f) : (a : L) → K) m : K) →
      ∀ (n : L),
        Membership.mem (α := K) J ((RingEquiv.symm (IsFractionRing.ringEquivOfRingEquiv f) : (a : L) → K) n : K) →
          HMul.hMul (α := K) (β := K) ((RingEquiv.symm (IsFractionRing.ringEquivOfRingEquiv f) : (a : L) → K) m : K)
              ((RingEquiv.symm (IsFractionRing.ringEquivOfRingEquiv f) : (a : L) → K) n : K) ∈
            (↑I : Submodule R K) * (↑J : Submodule R K)

Tactic:
exact fun m hm n hn ↦ Submodule.mul_mem_mul hm hn

Premises used: Submodule.mul_mem_mul
-- 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 :
  ∀ (x : L),
    Membership.mem (γ := 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 + J) : Submodule R K)) ⋯)
        x ↔
      x ∈
        HAdd.hAdd (α := 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)) ⋯)
⊢ 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)) ⋯ =
    HAdd.hAdd (α := 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:
ext x
-- 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
x : L
⊢ Membership.mem (γ := 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 + J) : Submodule R K)) ⋯)
      x ↔
    x ∈
      HAdd.hAdd (α := 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 [← mem_coe]

Premises used: FractionalIdeal.mem_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 : FractionalIdeal.{u_5, u_7} (R := R) R⁰ K
⊢ Eq.{u_8 + 1} (α := FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)
    (((ringEquivOfRingEquiv K L f :
            RingEquiv.{u_7, u_8} (FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
              (FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)) :
          (a : FractionalIdeal R⁰ K) → FractionalIdeal S⁰ L)
        I :
      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)) ⋯ :
      { I : Submodule S L // IsFractional S⁰ I })

Tactic:
rfl

Premises used: rfl
-- 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 : FractionalIdeal.{u_5, u_7} (R := R) R⁰ K
⊢ Eq (α := Submodule S L)
    (↑(((ringEquivOfRingEquiv K L f :
              RingEquiv.{u_7, u_8} (FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
                (FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)) :
            (a : FractionalIdeal R⁰ K) → FractionalIdeal S⁰ L)
          I) :
      Submodule S L)
    (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑I : Submodule R K))

Tactic:
rfl

Premises used: Submodule.map, rfl
-- 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
T : Type u_9
inst_10 : CommRing T
inst_11 : IsDomain T
M : Type u_10
inst_12 : CommRing M
inst_13 : Algebra T M
inst_14 : IsFractionRing T M
f : R ≃+* S
g : S ≃+* T
⊢ RingHomCompTriple (↑f : R →+* S) (↑g : S →+* T) (↑(f.trans g) : R →+* T)

Tactic:
have : RingHomCompTriple f (g : S →+* T) (f.trans g : R →+* T) := ⟨rfl⟩
-- 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
T : Type u_9
inst_10 : CommRing T
inst_11 : IsDomain T
M : Type u_10
inst_12 : CommRing M
inst_13 : Algebra T M
inst_14 : IsFractionRing T M
f : R ≃+* S
g : S ≃+* T
this : RingHomCompTriple (↑f : R →+* S) (↑g : S →+* T) (↑(f.trans g) : R →+* T)
h :
  ∀ (I : FractionalIdeal.{u_5, u_7} (R := R) R⁰ K),
    Eq.{u_10 + 1} (α := FractionalIdeal.{u_9, u_10} (R := T) T⁰ M)
      (((ringEquivOfRingEquiv K M (f.trans g) :
              RingEquiv.{u_7, u_10} (FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
                (FractionalIdeal.{u_9, u_10} (R := T) T⁰ M)) :
            (a : FractionalIdeal R⁰ K) → FractionalIdeal T⁰ M)
          I :
        FractionalIdeal.{u_9, u_10} (R := T) T⁰ M)
      (((RingEquiv.trans (S := FractionalIdeal.{u_6, u_8} (R := S) S⁰ L) (ringEquivOfRingEquiv K L f)
                (ringEquivOfRingEquiv L M g) :
              RingEquiv.{u_7, u_10} (FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
                (FractionalIdeal.{u_9, u_10} (R := T) T⁰ M)) :
            (a : FractionalIdeal R⁰ K) → FractionalIdeal T⁰ M)
          I :
        FractionalIdeal.{u_9, u_10} (R := T) T⁰ M)
⊢ Eq (α := RingEquiv.{u_7, u_10} (FractionalIdeal.{u_5, u_7} (R := R) R⁰ K) (FractionalIdeal.{u_9, u_10} (R := T) T⁰ M))
    (ringEquivOfRingEquiv K M (f.trans g))
    (RingEquiv.trans (S := FractionalIdeal.{u_6, u_8} (R := S) S⁰ L) (ringEquivOfRingEquiv K L f)
      (ringEquivOfRingEquiv L M g))

Tactic:
ext1 I
-- 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
T : Type u_9
inst_10 : CommRing T
inst_11 : IsDomain T
M : Type u_10
inst_12 : CommRing M
inst_13 : Algebra T M
inst_14 : IsFractionRing T M
f : R ≃+* S
g : S ≃+* T
this : RingHomCompTriple (↑f : R →+* S) (↑g : S →+* T) (↑(f.trans g) : R →+* T)
I : FractionalIdeal.{u_5, u_7} (R := R) R⁰ K
⊢ Eq.{u_10 + 1} (α := FractionalIdeal.{u_9, u_10} (R := T) T⁰ M)
    (((ringEquivOfRingEquiv K M (f.trans g) :
            RingEquiv.{u_7, u_10} (FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
              (FractionalIdeal.{u_9, u_10} (R := T) T⁰ M)) :
          (a : FractionalIdeal R⁰ K) → FractionalIdeal T⁰ M)
        I :
      FractionalIdeal.{u_9, u_10} (R := T) T⁰ M)
    (((RingEquiv.trans (S := FractionalIdeal.{u_6, u_8} (R := S) S⁰ L) (ringEquivOfRingEquiv K L f)
              (ringEquivOfRingEquiv L M g) :
            RingEquiv.{u_7, u_10} (FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
              (FractionalIdeal.{u_9, u_10} (R := T) T⁰ M)) :
          (a : FractionalIdeal R⁰ K) → FractionalIdeal T⁰ M)
        I :
      FractionalIdeal.{u_9, u_10} (R := T) T⁰ M)

Tactic:
simp only [ringEquivOfRingEquiv, RingEquiv.coe_ringHom_trans, Function.comp_apply,
    semilinearEquivOfRingEquiv_comp K L f M, LinearEquiv.coe_trans,
    Submodule.map_comp, RingEquiv.coe_mk, Equiv.coe_fn_mk, RingEquiv.coe_trans]

Premises used: RingEquiv.coe_ringHom_trans, RingEquiv.coe_mk, Submodule.map_comp, Equiv.coe_fn_mk, Function.comp_apply, RingEquiv.coe_trans, LinearEquiv.coe_trans, IsFractionRing.semilinearEquivOfRingEquiv_comp, FractionalIdeal.ringEquivOfRingEquiv
-- 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
T : Type u_9
inst_10 : CommRing T
inst_11 : IsDomain T
M : Type u_10
inst_12 : CommRing M
inst_13 : Algebra T M
inst_14 : IsFractionRing T M
f : R ≃+* S
g : S ≃+* T
I : FractionalIdeal.{u_5, u_7} (R := R) R⁰ K
⊢ Eq.{u_10 + 1} (α := FractionalIdeal.{u_9, u_10} (R := T) T⁰ M)
    (((ringEquivOfRingEquiv K M (f.trans g) :
            RingEquiv.{u_7, u_10} (FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
              (FractionalIdeal.{u_9, u_10} (R := T) T⁰ M)) :
          (a : FractionalIdeal R⁰ K) → FractionalIdeal T⁰ M)
        I :
      FractionalIdeal.{u_9, u_10} (R := T) T⁰ M)
    (((ringEquivOfRingEquiv L M g :
            RingEquiv.{u_8, u_10} (FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)
              (FractionalIdeal.{u_9, u_10} (R := T) T⁰ M)) :
          (a : FractionalIdeal S⁰ L) → FractionalIdeal T⁰ M)
        (((ringEquivOfRingEquiv K L f :
              RingEquiv.{u_7, u_8} (FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
                (FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)) :
            (a : FractionalIdeal R⁰ K) → FractionalIdeal S⁰ L)
          I) :
      FractionalIdeal.{u_9, u_10} (R := T) T⁰ M)

Tactic:
simp [ringEquivOfRingEquiv_trans K L M]

Premises used: FractionalIdeal.ringEquivOfRingEquiv_trans
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_5
K : Type u_7
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
h :
  ∀ (I : FractionalIdeal.{u_5, u_7} (R := R) R⁰ K) (x : K),
    Membership.mem (γ := FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
        ((ringEquivOfRingEquiv K K (RingEquiv.refl R) : (a : FractionalIdeal R⁰ K) → FractionalIdeal R⁰ K) I :
          FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
        x ↔
      Membership.mem (γ := FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
        ((RingEquiv.refl (FractionalIdeal.{u_5, u_7} (R := R) R⁰ K) : (a : FractionalIdeal R⁰ K) → FractionalIdeal R⁰ K)
            I :
          FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
        x
⊢ Eq (α := FractionalIdeal.{u_5, u_7} (R := R) R⁰ K ≃+* FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
    (ringEquivOfRingEquiv K K (RingEquiv.refl R)) (RingEquiv.refl (FractionalIdeal.{u_5, u_7} (R := R) R⁰ K))

Tactic:
ext I x
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_5
K : Type u_7
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
I : FractionalIdeal.{u_5, u_7} (R := R) R⁰ K
x : K
h :
  Membership.mem (γ := Submodule R K)
      (↑(Subtype.mk (p := fun (I : Submodule R K) ↦ IsFractional R⁰ I)
            (Submodule.map (↑(semilinearEquivOfRingEquiv K K (RingEquiv.refl R)) : K →ₗ[R] K) (↑I : Submodule R K)) ⋯) :
        Submodule R K)
      x ↔
    x ∈ (↑I : Submodule R K)
⊢ Membership.mem (γ := FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
      ((ringEquivOfRingEquiv K K (RingEquiv.refl R) : (a : FractionalIdeal R⁰ K) → FractionalIdeal R⁰ K) I :
        FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
      x ↔
    Membership.mem (γ := FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
      ((RingEquiv.refl (FractionalIdeal.{u_5, u_7} (R := R) R⁰ K) : (a : FractionalIdeal R⁰ K) → FractionalIdeal R⁰ K)
          I :
        FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
      x

Tactic:
simp only [ringEquivOfRingEquiv_apply, RingEquiv.coe_ringHom_refl, RingEquiv.symm_refl,
    val_eq_coe, RingEquiv.refl_apply, ← mem_coe]

Premises used: FractionalIdeal.ringEquivOfRingEquiv_apply, RingEquiv.coe_ringHom_refl, FractionalIdeal.mem_coe, FractionalIdeal.val_eq_coe, RingEquiv.refl_apply, RingEquiv.symm_refl
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_5
K : Type u_7
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
I : FractionalIdeal.{u_5, u_7} (R := R) R⁰ K
x : K
⊢ Membership.mem (γ := Submodule R K)
      (↑(Subtype.mk (p := fun (I : Submodule R K) ↦ IsFractional R⁰ I)
            (Submodule.map (↑(semilinearEquivOfRingEquiv K K (RingEquiv.refl R)) : K →ₗ[R] K) (↑I : Submodule R K)) ⋯) :
        Submodule R K)
      x ↔
    x ∈ (↑I : Submodule R K)

Tactic:
simp [semilinearEquivOfRingEquiv]

Premises used: IsFractionRing.semilinearEquivOfRingEquiv
-- 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
x : K
simp :
  Eq (α := 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) (R ∙ x)) ⋯)
    (spanSingleton S⁰ ((IsLocalization.map L (↑f : R →+* S) ⋯ : (a : K) → L) x))
⊢ Eq.{u_8 + 1} (α := FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)
    (((ringEquivOfRingEquiv K L f :
            RingEquiv.{u_7, u_8} (FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
              (FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)) :
          (a : FractionalIdeal R⁰ K) → FractionalIdeal S⁰ L)
        (spanSingleton R⁰ x) :
      FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)
    (spanSingleton S⁰ ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) x) :
      FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)

Tactic:
simp only [ringEquivOfRingEquiv, val_eq_coe, RingEquiv.symm_symm, RingEquiv.coe_mk,
    Equiv.coe_fn_mk, coe_spanSingleton, IsFractionRing.ringEquivOfRingEquiv_apply]

Premises used: IsFractionRing.ringEquivOfRingEquiv_apply, RingEquiv.coe_mk, Equiv.coe_fn_mk, RingEquiv.symm_symm, FractionalIdeal.coe_spanSingleton, FractionalIdeal.val_eq_coe, FractionalIdeal.ringEquivOfRingEquiv
-- 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
x : K
rw :
  ∀ (x_1 : L),
    Membership.mem (γ := 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) (R ∙ x)) ⋯)
        x_1 ↔
      Membership.mem (γ := FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)
        (spanSingleton S⁰ ((IsLocalization.map L (↑f : R →+* S) ⋯ : (a : K) → L) x) :
          FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)
        x_1
⊢ Eq (α := 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) (R ∙ x)) ⋯)
    (spanSingleton S⁰ ((IsLocalization.map L (↑f : R →+* S) ⋯ : (a : K) → L) x))

Tactic:
rw [SetLike.ext_iff]

Premises used: SetLike.ext_iff