awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
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 J : FractionalIdeal S P
C : P → Prop
r : P
hm : ∀ i ∈ I, ∀ j ∈ J, C (i * j)
ha : ∀ (x y : P), C x → C y → C (x + y)
hr : r ∈ Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) ((↑I : Submodule R P) * (↑J : Submodule R P)) ⋯
⊢ C r

Tactic:
exact Submodule.mul_induction_on hr hm ha
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
n : ℕ
zero : Eq.{u_2 + 1} (α := Submodule R P) (↑(Nat.unaryCast 0) : Submodule R P) (↑0 : Submodule R P)
succ :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := Submodule R P) (↑n.unaryCast : Submodule R P) (↑n : Submodule R P) →
      Eq.{u_2 + 1} (α := Submodule R P) (↑(n + 1).unaryCast : Submodule R P) (↑(n + 1) : Submodule R P)
⊢ Eq.{u_2 + 1} (α := Submodule R P) (↑n.unaryCast : Submodule R P) (↑n : Submodule R P)

Tactic:
induction n
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
⊢ Eq.{u_2 + 1} (α := Submodule R P) (↑(Nat.unaryCast 0) : Submodule R P) (↑0 : Submodule R P)

Tactic:
simp [*, Nat.unaryCast]

Premises used: Nat.unaryCast
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
n : ℕ
h : Eq.{u_2 + 1} (α := Submodule R P) (↑n.unaryCast : Submodule R P) (↑n : Submodule R P)
⊢ Eq.{u_2 + 1} (α := Submodule R P) (↑(n + 1).unaryCast : Submodule R P) (↑(n + 1) : Submodule R P)

Tactic:
simp [*, Nat.unaryCast]

Premises used: Nat.unaryCast
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
⊢ IsOrderedRing.{u_2} (FractionalIdeal S P)

Tactic:
CanonicallyOrderedAdd.toIsOrderedRing

Premises used: CanonicallyOrderedAdd.toIsOrderedRing
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
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 : Ideal R
⊢ LE.le.{u_2} (α := FractionalIdeal S P) (↑I : FractionalIdeal S P) 1

Tactic:
fun _ hx =>
  let ⟨y, _, hy⟩ := (mem_coeIdeal S).mp hx
  (mem_one_iff S).mpr ⟨y, hy⟩

Premises used: Iff.mpr, _private.0.FractionalIdeal.coeIdeal_le_one.match_1, FractionalIdeal.mem_one_iff, Membership.mem, FractionalIdeal.mem_coeIdeal, Exists.intro, Iff.mp, OfNat.ofNat
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
J : FractionalIdeal S P
mp : J ≤ 1 → ∃ (I : Ideal R), (↑I : FractionalIdeal S P) = J
mpr : (∃ (I : Ideal R), (↑I : FractionalIdeal S P) = J) → J ≤ 1
⊢ J ≤ 1 ↔ ∃ (I : Ideal R), (↑I : FractionalIdeal S P) = J

Tactic:
constructor
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
⊢ ∃ (I : Ideal R), (↑I : FractionalIdeal S P) = J

Tactic:
⟨⟨⟨⟨{ x : R | algebraMap R P x ∈ J }, ?_⟩, ?_⟩, ?_⟩, ?_⟩

Premises used: Algebra.algebraMap, setOf, Membership.mem, AddSubmonoid.mk, AddSubsemigroup.mk, Exists.intro, Submodule.mk, DFunLike.coe
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
mp :
  ∀ {a b : R},
    Membership.mem (γ := Set R) {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)} a →
      Membership.mem (γ := Set R) {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)} b →
        Membership.mem (γ := Set R) {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)} (a + b)
mp₁ :
  Membership.mem (γ := Set R)
    (AddSubsemigroup.carrier
      { carrier := {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)}, add_mem' := ⋯ })
    0
mp₂ :
  ∀ (c : R) {x : R},
    x ∈
        AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup
            { carrier := {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)}, add_mem' := ⋯,
              zero_mem' := ⋯ : AddSubmonoid R }) →
      c • x ∈
        AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup
            { carrier := {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)}, add_mem' := ⋯,
              zero_mem' := ⋯ : AddSubmonoid R })
mp₃ :
  (↑{ carrier := {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)}, add_mem' := ⋯,
          zero_mem' := ⋯, smul_mem' := ⋯ } :
      FractionalIdeal S P) =
    J
⊢ ∃ (I : Ideal R), (↑I : FractionalIdeal S P) = J

Tactic:
refine ⟨⟨⟨⟨{ x : R | algebraMap R P x ∈ J }, ?_⟩, ?_⟩, ?_⟩, ?_⟩
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
a b : R
ha : Membership.mem (γ := Set R) {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)} a
hb : Membership.mem (γ := Set R) {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)} b
mp : HAdd.hAdd (α := P) (β := P) ((algebraMap R P : (a : R) → P) a : P) ((algebraMap R P : (a : R) → P) b : P) ∈ J
⊢ Membership.mem (γ := Set R) {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)} (a + b)

Tactic:
rw [mem_setOf, map_add]

Premises used: map_add, Set.mem_setOf
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
a b : R
ha : Membership.mem (γ := Set R) {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)} a
hb : Membership.mem (γ := Set R) {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)} b
⊢ HAdd.hAdd (α := P) (β := P) ((algebraMap R P : (a : R) → P) a : P) ((algebraMap R P : (a : R) → P) b : P) ∈ J

Tactic:
J.val.add_mem ha hb

Premises used: Set.Mem, Subtype.val, Submodule.add_mem
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
a b : R
ha : Membership.mem (γ := Set R) {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)} a
hb : Membership.mem (γ := Set R) {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)} b
⊢ HAdd.hAdd (α := P) (β := P) ((algebraMap R P : (a : R) → P) a : P) ((algebraMap R P : (a : R) → P) b : P) ∈ J

Tactic:
exact J.val.add_mem ha hb

Premises used: Subtype.val, Submodule.add_mem
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
mp : 0 ∈ J
⊢ Membership.mem (γ := Set R)
    (AddSubsemigroup.carrier
      { carrier := {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)}, add_mem' := ⋯ })
    0

Tactic:
rw [mem_setOf, map_zero]

Premises used: map_zero, Set.mem_setOf
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
⊢ 0 ∈ J

Tactic:
J.zero_mem

Premises used: FractionalIdeal.zero_mem
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
⊢ 0 ∈ J

Tactic:
exact J.zero_mem

Premises used: FractionalIdeal.zero_mem
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
c x : R
hx :
  x ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        { carrier := {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)}, add_mem' := ⋯,
          zero_mem' := ⋯ : AddSubmonoid R })
mp : HSMul.hSMul (β := P) c ((algebraMap R P : (a : R) → P) x : P) ∈ J
⊢ c • x ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        { carrier := {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)}, add_mem' := ⋯,
          zero_mem' := ⋯ : AddSubmonoid R })

Tactic:
rw [smul_eq_mul, mem_setOf, map_mul, ← Algebra.smul_def]

Premises used: Set.mem_setOf, map_mul, Algebra.smul_def, smul_eq_mul
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
c x : R
hx :
  x ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        { carrier := {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)}, add_mem' := ⋯,
          zero_mem' := ⋯ : AddSubmonoid R })
⊢ HSMul.hSMul (β := P) c ((algebraMap R P : (a : R) → P) x : P) ∈ J

Tactic:
J.val.smul_mem c hx

Premises used: Set.Mem, Subtype.val, Submodule.smul_mem
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
c x : R
hx :
  x ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        { carrier := {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)}, add_mem' := ⋯,
          zero_mem' := ⋯ : AddSubmonoid R })
⊢ HSMul.hSMul (β := P) c ((algebraMap R P : (a : R) → P) x : P) ∈ J

Tactic:
exact J.val.smul_mem c hx

Premises used: Subtype.val, Submodule.smul_mem
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
mp :
  ∀ (x : P),
    Membership.mem (γ := FractionalIdeal S P)
        ((↑{ carrier := {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)}, add_mem' := ⋯,
                zero_mem' := ⋯, smul_mem' := ⋯ } :
            FractionalIdeal S P) :
          FractionalIdeal S P)
        x ↔
      x ∈ J
⊢ (↑{ carrier := {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)}, add_mem' := ⋯,
          zero_mem' := ⋯, smul_mem' := ⋯ } :
      FractionalIdeal S P) =
    J

Tactic:
ext x
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
x : P
mp :
  Membership.mem (γ := FractionalIdeal S P)
      ((↑{ carrier := {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)}, add_mem' := ⋯,
              zero_mem' := ⋯, smul_mem' := ⋯ } :
          FractionalIdeal S P) :
        FractionalIdeal S P)
      x →
    x ∈ J
mp₁ :
  x ∈ J →
    Membership.mem (γ := FractionalIdeal S P)
      ((↑{ carrier := {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)}, add_mem' := ⋯,
              zero_mem' := ⋯, smul_mem' := ⋯ } :
          FractionalIdeal S P) :
        FractionalIdeal S P)
      x
⊢ Membership.mem (γ := FractionalIdeal S P)
      ((↑{ carrier := {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)}, add_mem' := ⋯,
              zero_mem' := ⋯, smul_mem' := ⋯ } :
          FractionalIdeal S P) :
        FractionalIdeal S P)
      x ↔
    x ∈ J

Tactic:
constructor
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
x : P
y : R
hy :
  y ∈
    (↑{ carrier := {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)}, add_mem' := ⋯,
          zero_mem' := ⋯, smul_mem' := ⋯ : Submodule R R } :
      Set R)
eq_y : (Algebra.linearMap R P : (a : R) → P) y = x
mp mp₁ mp₂ mp₃ : Membership.mem (α := P) J ((Algebra.linearMap R P : (a : R) → P) y : P)
⊢ x ∈ J

Tactic:
rwa [← eq_y]
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
x : P
hx : x ∈ J
mp :
  ∀ (y : R) (hx : Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) y : P)),
    Membership.mem.{u_2, u_2} (α := P) (γ := FractionalIdeal S P)
      ((↑{ carrier := {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)}, add_mem' := ⋯,
              zero_mem' := ⋯, smul_mem' := ⋯ } :
          FractionalIdeal S P) :
        FractionalIdeal S P)
      ((algebraMap R P : (a : R) → P) y : P)
⊢ Membership.mem (γ := FractionalIdeal S P)
    ((↑{ carrier := {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)}, add_mem' := ⋯,
            zero_mem' := ⋯, smul_mem' := ⋯ } :
        FractionalIdeal S P) :
      FractionalIdeal S P)
    x

Tactic:
obtain ⟨y, rfl⟩ := (mem_one_iff S).mp (hJ hx)

Premises used: FractionalIdeal.mem_one_iff, Iff.mp, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
y : R
hx : Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) y : P)
⊢ Membership.mem.{u_2, u_2} (α := P) (γ := FractionalIdeal S P)
    ((↑{ carrier := {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)}, add_mem' := ⋯,
            zero_mem' := ⋯, smul_mem' := ⋯ } :
        FractionalIdeal S P) :
      FractionalIdeal S P)
    ((algebraMap R P : (a : R) → P) y : P)

Tactic:
mem_setOf.mpr ⟨y, hx, rfl⟩

Premises used: Iff.mpr, Set.Mem, setOf, Set.mem_setOf, And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
y : R
hx : Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) y : P)
⊢ Membership.mem.{u_2, u_2} (α := P) (γ := FractionalIdeal S P)
    ((↑{ carrier := {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)}, add_mem' := ⋯,
            zero_mem' := ⋯, smul_mem' := ⋯ } :
        FractionalIdeal S P) :
      FractionalIdeal S P)
    ((algebraMap R P : (a : R) → P) y : P)

Tactic:
exact mem_setOf.mpr ⟨y, hx, rfl⟩

Premises used: Iff.mpr, Set.mem_setOf
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
J : FractionalIdeal S P
I : Ideal R
hI : (↑I : FractionalIdeal S P) = J
mpr : LE.le.{u_2} (α := FractionalIdeal S P) (↑I : FractionalIdeal S P) 1
⊢ J ≤ 1

Tactic:
rw [← hI]
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
J : FractionalIdeal S P
I : Ideal R
hI : (↑I : FractionalIdeal S P) = J
⊢ LE.le.{u_2} (α := FractionalIdeal S P) (↑I : FractionalIdeal S P) 1

Tactic:
apply coeIdeal_le_one

Premises used: FractionalIdeal.coeIdeal_le_one
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
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
rw : (↑1 : Submodule R P) ≤ (↑I : Submodule R P) ↔ 1 ∈ I
rw₁ : 1 ≤ (↑I : Submodule R P) ↔ 1 ∈ I
rw₂ : 1 ∈ (↑I : Submodule R P) ↔ 1 ∈ I
rw₃ rw₄ : 1 ∈ I ↔ 1 ∈ I
⊢ 1 ≤ I ↔ 1 ∈ I

Tactic:
rw [← coe_le_coe, coe_one, Submodule.one_le, mem_coe]

Premises used: FractionalIdeal.coe_le_coe, FractionalIdeal.coe_one, FractionalIdeal.mem_coe, Submodule.one_le
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
rw : Eq.{u_2 + 1} (α := FractionalIdeal S P) (↑⊤ : FractionalIdeal S P) 1
rw₁ rw₂ : Eq.{u_2 + 1} (α := FractionalIdeal S P) 1 1
⊢ Eq.{u_2 + 1} (α := FractionalIdeal S P) (↑1 : FractionalIdeal S P) 1

Tactic:
rw [Ideal.one_eq_top, coeIdeal_top]

Premises used: FractionalIdeal.coeIdeal_top, Ideal.one_eq_top
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
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 : Ideal R
n : ℕ
⊢ (↑(I ^ n) : FractionalIdeal S P) = HPow.hPow (α := FractionalIdeal S P) (↑I : FractionalIdeal S P) n

Tactic:
(coeIdealHom S P).map_pow _ n

Premises used: Set.Mem, FractionalIdeal.coeIdeal, FractionalIdeal.coeIdealHom, RingHom.map_pow
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
α : Sort u_3
f : α → Ideal R
hS : S ≤ R⁰
⊢ Eq.{u_2 + 1} (α := FractionalIdeal S P) (↑(∏ᶠ (a : α), f a) : FractionalIdeal S P)
    (∏ᶠ (a : α), (↑(f a) : FractionalIdeal S P))

Tactic:
MonoidHom.map_finprod_of_injective (coeIdealHom S P).toMonoidHom (coeIdeal_injective' hS) f

Premises used: MonoidHom.map_finprod_of_injective, RingHom.toMonoidHom, FractionalIdeal.coeIdeal_injective', FractionalIdeal.coeIdeal, FractionalIdeal.coeIdealHom
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDomain R
S : Submonoid R
P : Type u_4
inst_2 : Nontrivial P
inst_3 : CommRing P
inst_4 : Algebra R P
inst_5 : Module.IsTorsionFree R P
hR : IsNoetherianRing R
hS : S ≤ R⁰
I : FractionalIdeal S P
⊢ FG I.num

Tactic:
have := hR.noetherian I.num
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDomain R
S : Submonoid R
P : Type u_4
inst_2 : Nontrivial P
inst_3 : CommRing P
inst_4 : Algebra R P
inst_5 : Module.IsTorsionFree R P
hR : IsNoetherianRing R
hS : S ≤ R⁰
I : FractionalIdeal S P
this : FG I.num
rw : ∀ (this : Module.Finite R ↥I.num), Module.Finite.{u_3, u_4} R ↥(↑I : Submodule R P)
⊢ (↑I : Submodule R P).FG

Tactic:
rw [← Module.Finite.iff_fg] at this ⊢

Premises used: Module.Finite.iff_fg
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDomain R
S : Submonoid R
P : Type u_4
inst_2 : Nontrivial P
inst_3 : CommRing P
inst_4 : Algebra R P
inst_5 : Module.IsTorsionFree R P
hR : IsNoetherianRing R
hS : S ≤ R⁰
I : FractionalIdeal S P
this : Module.Finite R ↥I.num
⊢ Module.Finite.{u_3, u_4} R ↥(↑I : Submodule R P)

Tactic:
.equiv (I.equivNum <| coe_ne_zero ⟨(I.den : R), hS (SetLike.coe_mem I.den)⟩).symm

Premises used: LinearEquiv.symm, SetLike.coe_mem, Subtype.mk, FractionalIdeal.den, FractionalIdeal.equivNum, nonZeroDivisors.coe_ne_zero, Module.Finite.equiv, Subtype.val
-- Module: Mathlib.RingTheory.FractionalIdeal.Basic
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDomain R
S : Submonoid R
P : Type u_4
inst_2 : Nontrivial P
inst_3 : CommRing P
inst_4 : Algebra R P
inst_5 : Module.IsTorsionFree R P
hR : IsNoetherianRing R
hS : S ≤ R⁰
I : FractionalIdeal S P
this : Module.Finite R ↥I.num
⊢ Module.Finite.{u_3, u_4} R ↥(↑I : Submodule R P)

Tactic:
exact .equiv (I.equivNum <| coe_ne_zero ⟨(I.den : R), hS (SetLike.coe_mem I.den)⟩).symm
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I_1 J I : FractionalIdeal M K
have :
  ∀ (a : A) (ha : a ∈ M) (frac : ∀ b ∈ (↑I : Submodule A K), IsInteger A (a • b)),
    IsFractional.{u_2, u_4} N (P := L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K)))
⊢ IsFractional.{u_2, u_4} N (P := L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K)))

Tactic:
have ⟨a, ha, frac⟩ := I.isFractional
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I_1 J I : FractionalIdeal M K
a : A
ha : a ∈ M
frac : ∀ b ∈ (↑I : Submodule A K), IsInteger A (a • b)
⊢ IsFractional.{u_2, u_4} N (P := L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K)))

Tactic:
⟨f a, hf ha, fun b hb ↦ ?_⟩

Premises used: IsFractional, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I_1 J I : FractionalIdeal M K
a : A
ha : a ∈ M
frac : ∀ b ∈ (↑I : Submodule A K), IsInteger A (a • b)
refine :
  ∀ (b : L)
    (hb :
      Membership.mem (γ := Submodule B L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))) b),
    IsInteger B (HSMul.hSMul.{u_2, u_4, u_4} (α := B) ((f : (a : A) → B) a : B) b)
⊢ IsFractional.{u_2, u_4} N (P := L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K)))

Tactic:
refine ⟨f a, hf ha, fun b hb ↦ ?_⟩
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I_1 J I : FractionalIdeal M K
a : A
ha : a ∈ M
frac : ∀ b ∈ (↑I : Submodule A K), IsInteger A (a • b)
b : L
hb : Membership.mem (γ := Submodule B L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))) b
⊢ (algebraMap B L : (a : B) → L) 0 = HSMul.hSMul.{u_2, u_4, u_4} (α := B) (β := L) ((f : (a : A) → B) a : B) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I_1 J I : FractionalIdeal M K
a : A
ha : a ∈ M
frac : ∀ b ∈ (↑I : Submodule A K), IsInteger A (a • b)
b : L
hb : Membership.mem (γ := Submodule B L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))) b
refine_1 :
  ∀ (x : L) (hx : Membership.mem (γ := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K)) x),
    IsInteger B (HSMul.hSMul.{u_2, u_4, u_4} (α := B) ((f : (a : A) → B) a : B) x)
refine_2 :
  ∀ (b : B) (c : L),
    Membership.mem (γ := Submodule B L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))) c →
      ∀ (hc : IsInteger B (HSMul.hSMul.{u_2, u_4, u_4} (α := B) ((f : (a : A) → B) a : B) c)),
        IsInteger B (HSMul.hSMul.{u_2, u_4, u_4} (α := B) ((f : (a : A) → B) a : B) (b • c))
⊢ IsInteger B (HSMul.hSMul.{u_2, u_4, u_4} (α := B) ((f : (a : A) → B) a : B) b)

Tactic:
refine span_induction (fun x hx ↦ ?_) ⟨0, by simp⟩
      (fun x y _ _ hx hy ↦ smul_add (f a) x y ▸ isInteger_add hx hy) (fun b c _ hc ↦ ?_) hb