awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FractionalIdeal.Norm
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
simp_rw :
  HDiv.hDiv (α := ℚ) (β := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) r : K)| : ℚ)
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
⊢ HDiv.hDiv (α := ℚ) (↑(Int.natAbs ((Algebra.norm ℤ : (a : R) → ℤ) r)) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑d : R)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|

Tactic:
simp_rw [Nat.cast_natAbs, Int.cast_abs, show ((Algebra.norm ℤ _) : ℚ) = algebraMap ℤ ℚ
      (Algebra.norm ℤ _) by rfl, ← Algebra.norm_localization ℤ ℤ⁰ (Sₘ := K) _]

Premises used: Int.cast_abs, Algebra.norm_localization, nonZeroDivisors, Nat.cast_natAbs, Int
-- Module: Mathlib.RingTheory.FractionalIdeal.Norm
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
rw : ¬(↑d : R) = 0
⊢ Ne (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) (0 : ℚ)

Tactic:
rw [ne_eq, abs_eq_zero, Algebra.norm_eq_zero_iff, IsFractionRing.to_map_eq_zero_iff]

Premises used: IsFractionRing.to_map_eq_zero_iff, ne_eq, abs_eq_zero, Algebra.norm_eq_zero_iff
-- Module: Mathlib.RingTheory.FractionalIdeal.Norm
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
⊢ ¬(↑d : R) = 0

Tactic:
nonZeroDivisors.coe_ne_zero _

Premises used: nonZeroDivisors.coe_ne_zero
-- Module: Mathlib.RingTheory.FractionalIdeal.Norm
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
⊢ ¬(↑d : R) = 0

Tactic:
exact nonZeroDivisors.coe_ne_zero _

Premises used: nonZeroDivisors.coe_ne_zero
-- Module: Mathlib.RingTheory.FractionalIdeal.Norm
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
rw :
  HDiv.hDiv (α := ℚ) (β := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((↑d : R) • x)| : ℚ)
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
rw₁ :
  HDiv.hDiv (α := ℚ) (β := ℚ)
      (|(Algebra.norm ℚ : (a : K) → ℚ) (HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) x)| : ℚ)
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
rw₂ :
  HDiv.hDiv (β := ℚ)
      |HMul.hMul (α := ℚ) (β := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K) : ℚ)
          ((Algebra.norm ℚ : (a : K) → ℚ) x : ℚ)|
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
rw₃ :
  HDiv.hDiv (β := ℚ)
      (HMul.hMul (α := ℚ) (β := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ)
        (|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℚ))
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
rw₄ :
  HMul.hMul (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ)
      (HDiv.hDiv (α := ℚ) (β := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℚ)
        (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ)) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
rw₅ rw₆ : Eq (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℚ)
⊢ HDiv.hDiv (α := ℚ) (β := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) r : K)| : ℚ)
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|

Tactic:
rw [hr, Algebra.smul_def, map_mul, abs_mul, mul_div_assoc, mul_div_cancel₀ _ (by
      rw [ne_eq, abs_eq_zero, Algebra.norm_eq_zero_iff, IsFractionRing.to_map_eq_zero_iff]
      exact nonZeroDivisors.coe_ne_zero _)]

Premises used: mul_div_assoc, abs_mul, mul_div_cancel₀, map_mul, Algebra.smul_def
-- Module: Mathlib.RingTheory.FractionalIdeal.Norm
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
h :
  ∀ (x_1 : K),
    x_1 ∈ HSMul.hSMul (β := Submodule R K) d (↑(spanSingleton R⁰ x) : Submodule R K) ↔
      Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
⊢ HSMul.hSMul (β := Submodule R K) d (↑(spanSingleton R⁰ x) : Submodule R K) =
    Submodule.map (Algebra.linearMap R K) (Ideal.span {r})

Tactic:
ext
-- Module: Mathlib.RingTheory.FractionalIdeal.Norm
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
x_1 : K
h :
  (∃ (b : K), Membership.mem (γ := Submodule R K) (↑(spanSingleton R⁰ x) : Submodule R K) b ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₁ :
  (∃ (b : K), Membership.mem (γ := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ x) b ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₂ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₃ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
    ∃ (y : R), Membership.mem (γ := Submodule R R) (Ideal.span {r}) y ∧ (Algebra.linearMap R K : (a : R) → K) y = x_1
h₄ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
    ∃ (y : R), Membership.mem (γ := Submodule R R) (Ideal.span {r}) y ∧ (algebraMap R K : (a : R) → K) y = x_1
h₅ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ (↑d : R) • b = x_1) ↔
    ∃ (y : R), Membership.mem (γ := Submodule R R) (Ideal.span {r}) y ∧ (algebraMap R K : (a : R) → K) y = x_1
h₆ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ (↑d : R) • b = x_1) ↔
    ∃ (y : R), (∃ (a : R), a * r = y) ∧ (algebraMap R K : (a : R) → K) y = x_1
h₇ : (∃ (a : R), (↑d : R) • a • x = x_1) ↔ ∃ (a : R), (algebraMap R K : (a : R) → K) (a * r) = x_1
h₈ :
  (∃ (a : R), (↑d : R) • a • x = x_1) ↔
    ∃ (a : R),
      HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) a : K) ((algebraMap R K : (a : R) → K) r : K) = x_1
h₉ :
  (∃ (a : R), (↑d : R) • a • x = x_1) ↔
    ∃ (a : R), HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) a : K) ((↑d : R) • x) = x_1
h₁₀ : (∃ (a : R), (↑d : R) • a • x = x_1) ↔ ∃ (a : R), a • (↑d : R) • x = x_1
⊢ x_1 ∈ HSMul.hSMul (β := Submodule R K) d (↑(spanSingleton R⁰ x) : Submodule R K) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1

Tactic:
simp_rw [Submodule.mem_smul_pointwise_iff_exists, mem_coe, mem_spanSingleton, Submodule.mem_map,
      Algebra.linearMap_apply, Submonoid.smul_def, Ideal.mem_span_singleton', exists_exists_eq_and,
      map_mul, hr, ← Algebra.smul_def, smul_comm (d : R)]

Premises used: Ideal.mem_span_singleton', Submodule.mem_map, Algebra.linearMap_apply, FractionalIdeal.mem_spanSingleton, Submonoid.smul_def, Submodule.mem_smul_pointwise_iff_exists, map_mul, exists_exists_eq_and, FractionalIdeal.mem_coe, Algebra.smul_def, SMulCommClass.smul_comm, Subtype.val
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
g : P →ₐ[R] P'
I : Submodule R P
a : R
a_nonzero : a ∈ S
hI : ∀ b ∈ I, IsInteger R (a • b)
b : P'
hb : b ∈ Submodule.map g.toLinearMap I
obtain : ∀ (b' : P) (b'_mem : b' ∈ I) (hb' : (g.toLinearMap : (a : P) → P') b' = b), IsInteger R (a • b)
⊢ IsInteger R (a • b)

Tactic:
obtain ⟨b', b'_mem, hb'⟩ := Submodule.mem_map.mp hb

Premises used: Submodule.mem_map, Iff.mp
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
g : P →ₐ[R] P'
I : Submodule R P
a : R
a_nonzero : a ∈ S
hI : ∀ b ∈ I, IsInteger R (a • b)
b : P'
hb : b ∈ Submodule.map g.toLinearMap I
b' : P
b'_mem : b' ∈ I
hb' : (g.toLinearMap : (a : P) → P') b' = b
⊢ (g : (a : P) → P') b' = b

Tactic:
rw [AlgHom.toLinearMap_apply] at hb'

Premises used: AlgHom.toLinearMap_apply
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
g : P →ₐ[R] P'
I : Submodule R P
a : R
a_nonzero : a ∈ S
hI : ∀ b ∈ I, IsInteger R (a • b)
b : P'
hb : b ∈ Submodule.map g.toLinearMap I
b' : P
b'_mem : b' ∈ I
hb' : (g : (a : P) → P') b' = b
obtain : ∀ (x : R) (hx : (algebraMap R P : (a : R) → P) x = a • b'), IsInteger R (a • b)
⊢ IsInteger R (a • b)

Tactic:
obtain ⟨x, hx⟩ := hI b' b'_mem
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
g : P →ₐ[R] P'
I : Submodule R P
a : R
a_nonzero : a ∈ S
hI : ∀ b ∈ I, IsInteger R (a • b)
b : P'
hb : b ∈ Submodule.map g.toLinearMap I
b' : P
b'_mem : b' ∈ I
hb' : (g : (a : P) → P') b' = b
x : R
hx : (algebraMap R P : (a : R) → P) x = a • b'
h : (algebraMap R P' : (a : R) → P') x = a • b
⊢ IsInteger R (a • b)

Tactic:
use x
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
g : P →ₐ[R] P'
I : Submodule R P
a : R
a_nonzero : a ∈ S
hI : ∀ b ∈ I, IsInteger R (a • b)
b : P'
hb : b ∈ Submodule.map g.toLinearMap I
b' : P
b'_mem : b' ∈ I
hb' : (g : (a : P) → P') b' = b
x : R
hx : (algebraMap R P : (a : R) → P) x = a • b'
h : (g : (a : P) → P') ((algebraMap R P : (a : R) → P) x : P) = a • b
h₁ : (g : (a : P) → P') (a • b') = a • b
h₂ : HSMul.hSMul (β := P') a ((g : (a : P) → P') b' : P') = a • b
h₃ h₄ : a • b = a • b
⊢ (algebraMap R P' : (a : R) → P') x = a • b

Tactic:
rw [← g.commutes, hx, map_smul, hb']

Premises used: AlgHom.commutes, map_smul
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
g : P →ₐ[R] P'
I : FractionalIdeal S P
⊢ (↑(map g I) : Submodule R P') = Submodule.map g.toLinearMap (↑I : Submodule R P)

Tactic:
rfl

Premises used: FractionalIdeal.coeToSubmodule, Submodule.map, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
I : FractionalIdeal S P
g : P →ₐ[R] P'
y : P'
⊢ y ∈ map g I ↔ ∃ x ∈ I, (g : (a : P) → P') x = y

Tactic:
Submodule.mem_map

Premises used: Set.Mem, Submodule.mem_map
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : FractionalIdeal S P
⊢ map (AlgHom.id R P) I = I

Tactic:
coeToSubmodule_injective (Submodule.map_id (I : Submodule R P))

Premises used: Submodule.map_id, FractionalIdeal.coeToSubmodule, FractionalIdeal.coeToSubmodule_injective
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
P'' : Type u_4
inst_5 : CommRing P''
inst_6 : Algebra R P''
I : FractionalIdeal S P
g : P →ₐ[R] P'
g' : P' →ₐ[R] P''
⊢ map (g'.comp g) I = map g' (map g I)

Tactic:
coeToSubmodule_injective (Submodule.map_comp g.toLinearMap g'.toLinearMap I)

Premises used: AlgHom.toLinearMap, Submodule.map_comp, FractionalIdeal.coeToSubmodule, FractionalIdeal.coeToSubmodule_injective
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
g : P →ₐ[R] P'
I : Ideal R
a :
  ∀ (x : P'),
    Membership.mem (γ := FractionalIdeal S P') (map g (↑I : FractionalIdeal S P)) x ↔
      Membership.mem (γ := FractionalIdeal S P') (↑I : FractionalIdeal S P') x
⊢ Eq (α := FractionalIdeal S P') (map g (↑I : FractionalIdeal S P)) (↑I : FractionalIdeal S P')

Tactic:
ext x
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
g : P →ₐ[R] P'
I : Ideal R
x : P'
⊢ Membership.mem (γ := FractionalIdeal S P') (map g (↑I : FractionalIdeal S P)) x ↔
    Membership.mem (γ := FractionalIdeal S P') (↑I : FractionalIdeal S P') x

Tactic:
simp
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
g : P →ₐ[R] P'
⊢ Eq (α := FractionalIdeal S P') (map g 1) 1

Tactic:
map_coeIdeal g ⊤

Premises used: FractionalIdeal.map_coeIdeal, Top.top
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
g : P →ₐ[R] P'
⊢ Eq (α := FractionalIdeal S P') (map g 0) 0

Tactic:
map_coeIdeal g 0

Premises used: FractionalIdeal.map_coeIdeal, OfNat.ofNat
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
I J : FractionalIdeal S P
g : P →ₐ[R] P'
⊢ map g (I + J) = map g I + map g J

Tactic:
coeToSubmodule_injective (Submodule.map_sup _ _ _)

Premises used: Submodule.map_sup, FractionalIdeal.coeToSubmodule_injective
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
I J : FractionalIdeal S P
g : P →ₐ[R] P'
simp :
  map g (Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) ((↑I : Submodule R P) * (↑J : Submodule R P)) ⋯) =
    Subtype.mk (p := fun (I : Submodule R P') ↦ IsFractional S I)
      ((↑(map g I) : Submodule R P') * (↑(map g J) : Submodule R P')) ⋯
⊢ map g (I * J) = map g I * map g J

Tactic:
simp only [mul_def]

Premises used: FractionalIdeal.mul_def
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
I J : FractionalIdeal S P
g : P →ₐ[R] P'
⊢ map g (Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) ((↑I : Submodule R P) * (↑J : Submodule R P)) ⋯) =
    Subtype.mk (p := fun (I : Submodule R P') ↦ IsFractional S I)
      ((↑(map g I) : Submodule R P') * (↑(map g J) : Submodule R P')) ⋯

Tactic:
coeToSubmodule_injective (Submodule.map_mul _ _ _)

Premises used: Submodule.map_mul, FractionalIdeal.coeToSubmodule_injective
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
I J : FractionalIdeal S P
g : P →ₐ[R] P'
⊢ map g (Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) ((↑I : Submodule R P) * (↑J : Submodule R P)) ⋯) =
    Subtype.mk (p := fun (I : Submodule R P') ↦ IsFractional S I)
      ((↑(map g I) : Submodule R P') * (↑(map g J) : Submodule R P')) ⋯

Tactic:
exact coeToSubmodule_injective (Submodule.map_mul _ _ _)
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
I : FractionalIdeal S P
g : P ≃ₐ[R] P'
rw : map ((↑g.symm : P' →ₐ[R] P).comp (↑g : P →ₐ[R] P')) I = I
rw₁ : map (AlgHom.id R P) I = I
rw₂ rw₃ : I = I
⊢ map (↑g.symm : P' →ₐ[R] P) (map (↑g : P →ₐ[R] P') I) = I

Tactic:
rw [← map_comp, g.symm_comp, map_id]

Premises used: FractionalIdeal.map_comp, FractionalIdeal.map_id, AlgEquiv.symm_comp
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
I : FractionalIdeal S P'
g : P ≃ₐ[R] P'
rw : map ((↑g : P →ₐ[R] P').comp (↑g.symm : P' →ₐ[R] P)) I = I
rw₁ : map (AlgHom.id R P') I = I
rw₂ rw₃ : I = I
⊢ map (↑g : P →ₐ[R] P') (map (↑g.symm : P' →ₐ[R] P) I) = I

Tactic:
rw [← map_comp, g.comp_symm, map_id]

Premises used: FractionalIdeal.map_comp, FractionalIdeal.map_id, AlgEquiv.comp_symm
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
f : P →ₐ[R] P'
h : Function.Injective.{u_2 + 1, u_3 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
x : P
I : FractionalIdeal S P
⊢ Membership.mem (α := P') (map f I) ((f : (a : P) → P') x : P') ↔ x ∈ I

Tactic:
mem_map.trans ⟨fun ⟨_, hx', x'_eq⟩ => h x'_eq ▸ hx', fun h => ⟨x, h, rfl⟩⟩

Premises used: FractionalIdeal.mem_map, Membership.mem, Eq.rec, _private.0.FractionalIdeal.map_mem_map.match_1, And.intro, Iff.intro, Exists.intro, Iff.trans, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
f : P →ₐ[R] P'
h : Function.Injective.{u_2 + 1, u_3 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
⊢ Function.Injective (α := FractionalIdeal S P) (map f)

Tactic:
fun _ _ hIJ =>
  ext fun _ => (map_mem_map h).symm.trans (hIJ.symm ▸ map_mem_map h)

Premises used: Eq.rec, FractionalIdeal.ext, Iff.trans, Function.Injective, Eq.symm, Iff.symm, FractionalIdeal.map_mem_map
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
P'' : Type u_4
inst_5 : CommRing P''
inst_6 : Algebra R P''
I_1 J : FractionalIdeal S P
g_1 : P →ₐ[R] P'
g : P ≃ₐ[R] P'
I : FractionalIdeal S P
rw : map ((↑g.symm : P' →ₐ[R] P).comp (↑g : P →ₐ[R] P')) I = I
rw₁ : map (AlgHom.id R P) I = I
rw₂ rw₃ : I = I
⊢ map (↑g.symm : P' →ₐ[R] P) (map (↑g : P →ₐ[R] P') I) = I

Tactic:
rw [← map_comp, AlgEquiv.symm_comp, map_id]

Premises used: FractionalIdeal.map_comp, FractionalIdeal.map_id, AlgEquiv.symm_comp
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
P'' : Type u_4
inst_5 : CommRing P''
inst_6 : Algebra R P''
I_1 J : FractionalIdeal S P
g_1 : P →ₐ[R] P'
g : P ≃ₐ[R] P'
I : FractionalIdeal S P'
rw : map ((↑g : P →ₐ[R] P').comp (↑g.symm : P' →ₐ[R] P)) I = I
rw₁ : map (AlgHom.id R P') I = I
rw₂ rw₃ : I = I
⊢ map (↑g : P →ₐ[R] P') (map (↑g.symm : P' →ₐ[R] P) I) = I

Tactic:
rw [← map_comp, AlgEquiv.comp_symm, map_id]

Premises used: FractionalIdeal.map_comp, FractionalIdeal.map_id, AlgEquiv.comp_symm
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
g : P ≃ₐ[R] P'
⊢ Eq (α := (a : FractionalIdeal S P) → FractionalIdeal S P')
    (⇑(mapEquiv g) : (a : FractionalIdeal S P) → FractionalIdeal S P') (map (↑g : P →ₐ[R] P'))

Tactic:
rfl

Premises used: FractionalIdeal.map, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
g : P ≃ₐ[R] P'
I : FractionalIdeal S P
⊢ ((mapEquiv g : RingEquiv.{u_2, u_3} (FractionalIdeal S P) (FractionalIdeal S P')) :
        (a : FractionalIdeal S P) → FractionalIdeal S P')
      I =
    map (↑g : P →ₐ[R] P') I

Tactic:
rfl

Premises used: FractionalIdeal.map, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
g : P ≃ₐ[R] P'
⊢ Eq (α := RingEquiv.{u_3, u_2} (FractionalIdeal S P') (FractionalIdeal S P)) (RingEquiv.symm (mapEquiv g))
    (mapEquiv g.symm)

Tactic:
rfl

Premises used: AlgEquiv.symm, FractionalIdeal.mapEquiv, FractionalIdeal.map, Equiv.symm, RingEquiv.symm, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
x : FractionalIdeal S P
⊢ Eq (α := FractionalIdeal S P)
    ((mapEquiv AlgEquiv.refl : (a : FractionalIdeal S P) → FractionalIdeal S P) x : FractionalIdeal S P)
    ((RingEquiv.refl (FractionalIdeal S P) : (a : FractionalIdeal S P) → FractionalIdeal S P) x : FractionalIdeal S P)

Tactic:
simp
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
s : Set P
h_1 : ∃ a ∈ S, ∀ b ∈ s, IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ b ∈ s, IsInteger R (a • b)
x : P
hb : Membership.mem (γ := Submodule R P) (span R s) x
rw : IsInteger.{u_1, u_2} R (S := P) 0
⊢ IsInteger R (HSMul.hSMul (β := P) a 0)

Tactic:
rw [smul_zero]

Premises used: smul_zero