awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
f : R →+* S
⊢ Eq.{u_2 + 1} (α := S)
    ((coeff (single 1 1) : (a : MvPowerSeries (Fin 2) S) → S)
        (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 2) R) (MvPowerSeries (Fin 2) S)) :
              (a : MvPowerSeries (Fin 2) R) → MvPowerSeries (Fin 2) S)
            F.toPowerSeries :
          MvPowerSeries (Fin 2) S) :
      S)
    (1 : S)

Tactic:
simp [F.lin_coeff_Y]

Premises used: FormalGroup.lin_coeff_Y
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
f : R →+* S
g₁ g₂ : MvPowerSeries (Fin 3) R
h :
  ∀ (i : Fin (Nat.succ 0).succ),
    Eq.{u_2 + 1} (α := MvPowerSeries (Fin 3) S)
      (![((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
                (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
              g₁,
            ((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
                (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
              g₂]
          i :
        MvPowerSeries (Fin 3) S)
      (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
            (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
          (![g₁, g₂] i) :
        MvPowerSeries (Fin 3) S)
⊢ Eq.{u_2 + 1} (α := Fin (Nat.succ 0).succ → MvPowerSeries (Fin 3) S)
    (![((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
            (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
          g₁,
        ((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
            (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
          g₂] :
      Fin (Nat.succ 0).succ → MvPowerSeries (Fin 3) S)
    fun (i : Fin (Nat.succ 0).succ) ↦
    (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
          (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
        (![g₁, g₂] i) :
      MvPowerSeries (Fin 3) S)

Tactic:
ext1 i
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
f : R →+* S
g₁ g₂ : MvPowerSeries (Fin 3) R
i : Fin (Nat.succ 0).succ
h :
  Eq.{u_2 + 1} (α := MvPowerSeries (Fin 3) S)
    (Matrix.vecCons (n := Nat.succ 0)
        (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
            (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
          g₁)
        ![((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
              (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
            g₂]
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) :
      MvPowerSeries (Fin 3) S)
    (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
          (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
        (![g₁, g₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)) :
      MvPowerSeries (Fin 3) S)
h₁ :
  Eq.{u_2 + 1} (α := MvPowerSeries (Fin 3) S)
    (Matrix.vecCons (n := Nat.succ 0)
        (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
            (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
          g₁)
        ![((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
              (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
            g₂]
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩) :
      MvPowerSeries (Fin 3) S)
    (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
          (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
        (![g₁, g₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)) :
      MvPowerSeries (Fin 3) S)
⊢ Eq.{u_2 + 1} (α := MvPowerSeries (Fin 3) S)
    (![((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
              (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
            g₁,
          ((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
              (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
            g₂]
        i :
      MvPowerSeries (Fin 3) S)
    (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
          (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
        (![g₁, g₂] i) :
      MvPowerSeries (Fin 3) S)

Tactic:
fin_cases i
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
f : R →+* S
g₁ g₂ : MvPowerSeries (Fin 3) R
⊢ Eq.{u_2 + 1} (α := MvPowerSeries (Fin 3) S)
    (Matrix.vecCons (n := Nat.succ 0)
        (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
            (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
          g₁)
        ![((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
              (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
            g₂]
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) :
      MvPowerSeries (Fin 3) S)
    (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
          (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
        (![g₁, g₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)) :
      MvPowerSeries (Fin 3) S)

Tactic:
simp
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
f : R →+* S
g₁ g₂ : MvPowerSeries (Fin 3) R
⊢ Eq.{u_2 + 1} (α := MvPowerSeries (Fin 3) S)
    (Matrix.vecCons (n := Nat.succ 0)
        (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
            (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
          g₁)
        ![((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
              (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
            g₂]
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩) :
      MvPowerSeries (Fin 3) S)
    (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
          (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
        (![g₁, g₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)) :
      MvPowerSeries (Fin 3) S)

Tactic:
simp
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
f : R →+* S
⊢ ∀ (g₁ g₂ : MvPowerSeries (Fin 3) R),
    Eq.{u_2 + 1} (α := Fin (Nat.succ 0).succ → MvPowerSeries (Fin 3) S)
      (![((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
              (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
            g₁,
          ((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
              (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
            g₂] :
        Fin (Nat.succ 0).succ → MvPowerSeries (Fin 3) S)
      fun (i : Fin (Nat.succ 0).succ) ↦
      (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 3) R) (MvPowerSeries (Fin 3) S)) :
            (a : MvPowerSeries (Fin 3) R) → MvPowerSeries (Fin 3) S)
          (![g₁, g₂] i) :
        MvPowerSeries (Fin 3) S)

Tactic:
have (g₁ g₂ : MvPowerSeries (Fin 3) R) : ![g₁.map f, g₂.map f] =
      fun i => (![g₁, g₂] i).map f := by ext1 i; fin_cases i <;> simp
-- 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
⊢ IsFractional S (↑I : Submodule R P)

Tactic:
I.prop

Premises used: FractionalIdeal.coeToSubmodule, Subtype.prop
-- 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 :
  Subtype.mk (p := fun (x : R) ↦ x ∈ S)
        (Exists.choose (p := fun (a : R) ↦ a ∈ S ∧ ∀ b ∈ (↑I : Submodule R P), IsInteger R (a • b)) ⋯) ⋯ •
      (↑I : Submodule R P) =
    LinearMap.range (Algebra.linearMap R P) ⊓ I.den • (↑I : Submodule R P)
⊢ I.den • (↑I : Submodule R P) = Submodule.map (Algebra.linearMap R P) I.num

Tactic:
rw [den, num, Submodule.map_comap_eq]

Premises used: FractionalIdeal.num, Submodule.map_comap_eq, FractionalIdeal.den
-- 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
⊢ Subtype.mk (p := fun (x : R) ↦ x ∈ S)
        (Exists.choose (p := fun (a : R) ↦ a ∈ S ∧ ∀ b ∈ (↑I : Submodule R P), IsInteger R (a • b)) ⋯) ⋯ •
      (↑I : Submodule R P) =
    LinearMap.range (Algebra.linearMap R P) ⊓ I.den • (↑I : Submodule R P)

Tactic:
(inf_of_le_right ?_).symm

Premises used: inf_of_le_right, Eq.symm
-- 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
refine :
  Subtype.mk (p := fun (x : R) ↦ x ∈ S)
        (Exists.choose (p := fun (a : R) ↦ a ∈ S ∧ ∀ b ∈ (↑I : Submodule R P), IsInteger R (a • b)) ⋯) ⋯ •
      (↑I : Submodule R P) ≤
    LinearMap.range (Algebra.linearMap R P)
⊢ Subtype.mk (p := fun (x : R) ↦ x ∈ S)
        (Exists.choose (p := fun (a : R) ↦ a ∈ S ∧ ∀ b ∈ (↑I : Submodule R P), IsInteger R (a • b)) ⋯) ⋯ •
      (↑I : Submodule R P) =
    LinearMap.range (Algebra.linearMap R P) ⊓ I.den • (↑I : Submodule R P)

Tactic:
refine (inf_of_le_right ?_).symm

Premises used: inf_of_le_right, Eq.symm
-- 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
a : P
ha : a ∈ (↑(↑I : Submodule R P) : Set P)
⊢ Membership.mem (α := P) (γ := Submodule R P) (LinearMap.range (Algebra.linearMap R P))
    ((DistribSMul.toLinearMap R P
            (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S)
                  (Exists.choose (p := fun (a : R) ↦ a ∈ S ∧ ∀ b ∈ (↑I : Submodule R P), IsInteger R (a • b)) ⋯) ⋯) :
              R) :
          (a : P) → P)
        a :
      P)

Tactic:
I.2.choose_spec.2 a ha

Premises used: IsLocalization.IsInteger, Exists.choose_spec, Set.Mem, And.right, Classical.choose, Subtype.property
-- 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
a : P
ha : a ∈ (↑(↑I : Submodule R P) : Set P)
⊢ Membership.mem (α := P) (γ := Submodule R P) (LinearMap.range (Algebra.linearMap R P))
    ((DistribSMul.toLinearMap R P
            (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S)
                  (Exists.choose (p := fun (a : R) ↦ a ∈ S ∧ ∀ b ∈ (↑I : Submodule R P), IsInteger R (a • b)) ⋯) ⋯) :
              R) :
          (a : P) → P)
        a :
      P)

Tactic:
exact I.2.choose_spec.2 a ha

Premises used: Exists.choose_spec, And.right, Subtype.property
-- 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 : FaithfulSMul R P
I : FractionalIdeal S P
reg : IsSMulRegular P I.den
refine_1 :
  ∀ (x : P) (hx : x ∈ (↑I : Submodule R P)),
    Membership.mem (α := P) (γ := Submodule R P) (Submodule.map (Algebra.linearMap R P) I.num)
      ((DistribSMul.toLinearMap R P I.den : (a : P) → P) x : P)
refine_2 :
  ∀ (x x_1 : ↥(↑I : Submodule R P))
    (hxy :
      Eq (α := ↥(Submodule.map (Algebra.linearMap R P) I.num))
        ((LinearMap.restrict (DistribSMul.toLinearMap R P I.den) ⋯ :
              (a : ↥(↑I : Submodule R P)) → ↥(Submodule.map (Algebra.linearMap R P) I.num))
            x :
          ↥(Submodule.map (Algebra.linearMap R P) I.num))
        ((LinearMap.restrict (DistribSMul.toLinearMap R P I.den) ⋯ :
              (a : ↥(↑I : Submodule R P)) → ↥(Submodule.map (Algebra.linearMap R P) I.num))
            x_1 :
          ↥(Submodule.map (Algebra.linearMap R P) I.num))),
    x = x_1
refine_3 :
  ∀ (x : ↥(Submodule.map (Algebra.linearMap R P) I.num)) (y : P)
    (hy : Membership.mem (γ := Submodule R P) (Submodule.map (Algebra.linearMap R P) I.num) y),
    ∃ (a : ↥(↑I : Submodule R P)),
      (LinearMap.restrict (DistribSMul.toLinearMap R P I.den) ⋯ :
            (a : ↥(↑I : Submodule R P)) → ↥(Submodule.map (Algebra.linearMap R P) I.num))
          a =
        Subtype.mk (p := fun (x : P) ↦
          Membership.mem (γ := Submodule R P) (Submodule.map (Algebra.linearMap R P) I.num) x) y hy
⊢ LinearEquiv.{u_1, u_1, u_2, u_1} (RingHom.id R) ↥(↑I : Submodule R P) ↥I.num

Tactic:
refine LinearEquiv.trans
    (LinearEquiv.ofBijective ((DistribSMul.toLinearMap R P I.den).restrict fun _ hx ↦ ?_)
      ⟨fun _ _ hxy ↦ ?_, fun ⟨y, hy⟩ ↦ ?_⟩)
    (Submodule.equivMapOfInjective (Algebra.linearMap R P)
      (FaithfulSMul.algebraMap_injective R P) (num I)).symm

Premises used: FractionalIdeal.num, LinearEquiv.symm, DistribSMul.toLinearMap, Submodule.equivMapOfInjective, LinearMap.restrict, Algebra.linearMap, FractionalIdeal.den, FaithfulSMul.algebraMap_injective, And.intro, LinearEquiv.trans, LinearEquiv.ofBijective
-- 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 : FaithfulSMul R P
I : FractionalIdeal S P
reg : IsSMulRegular P I.den
x : P
hx : x ∈ (↑I : Submodule R P)
refine_1 :
  Membership.mem (α := P) (I.den • (↑I : Submodule R P)) ((DistribSMul.toLinearMap R P I.den : (a : P) → P) x : P)
⊢ Membership.mem (α := P) (γ := Submodule R P) (Submodule.map (Algebra.linearMap R P) I.num)
    ((DistribSMul.toLinearMap R P I.den : (a : P) → P) x : P)

Tactic:
rw [← den_mul_self_eq_num]

Premises used: FractionalIdeal.den_mul_self_eq_num
-- 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 : FaithfulSMul R P
I : FractionalIdeal S P
reg : IsSMulRegular P I.den
x : P
hx : x ∈ (↑I : Submodule R P)
⊢ Membership.mem (α := P) (I.den • (↑I : Submodule R P)) ((DistribSMul.toLinearMap R P I.den : (a : P) → P) x : P)

Tactic:
Submodule.smul_mem_pointwise_smul _ _ _ hx

Premises used: Set.Mem, Submodule.smul_mem_pointwise_smul
-- 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 : FaithfulSMul R P
I : FractionalIdeal S P
reg : IsSMulRegular P I.den
x : P
hx : x ∈ (↑I : Submodule R P)
⊢ Membership.mem (α := P) (I.den • (↑I : Submodule R P)) ((DistribSMul.toLinearMap R P I.den : (a : P) → P) x : P)

Tactic:
exact Submodule.smul_mem_pointwise_smul _ _ _ hx

Premises used: Submodule.smul_mem_pointwise_smul
-- 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 : FaithfulSMul R P
I : FractionalIdeal S P
reg : IsSMulRegular P I.den
x x_1 : ↥(↑I : Submodule R P)
hxy :
  Eq (α := ↥(Submodule.map (Algebra.linearMap R P) I.num))
    ((LinearMap.restrict (DistribSMul.toLinearMap R P I.den) ⋯ :
          (a : ↥(↑I : Submodule R P)) → ↥(Submodule.map (Algebra.linearMap R P) I.num))
        x :
      ↥(Submodule.map (Algebra.linearMap R P) I.num))
    ((LinearMap.restrict (DistribSMul.toLinearMap R P I.den) ⋯ :
          (a : ↥(↑I : Submodule R P)) → ↥(Submodule.map (Algebra.linearMap R P) I.num))
        x_1 :
      ↥(Submodule.map (Algebra.linearMap R P) I.num))
⊢ x = x_1

Tactic:
simpa [LinearMap.restrict_apply, reg.eq_iff] using hxy

Premises used: Function.Injective.eq_iff, LinearMap.restrict_apply
-- 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 : FaithfulSMul R P
I : FractionalIdeal S P
reg : IsSMulRegular P I.den
x : ↥(Submodule.map (Algebra.linearMap R P) I.num)
y : P
hy : Membership.mem (γ := Submodule R P) (Submodule.map (Algebra.linearMap R P) I.num) y
⊢ y ∈ I.den • (↑I : Submodule R P)

Tactic:
rw [← den_mul_self_eq_num] at hy

Premises used: FractionalIdeal.den_mul_self_eq_num
-- 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 : FaithfulSMul R P
I : FractionalIdeal S P
reg : IsSMulRegular P I.den
x : ↥(Submodule.map (Algebra.linearMap R P) I.num)
y : P
hy_1 : Membership.mem (γ := Submodule R P) (Submodule.map (Algebra.linearMap R P) I.num) y
hy : y ∈ I.den • (↑I : Submodule R P)
refine_3 :
  ∀ (x : P) (hx : x ∈ (↑(↑I : Submodule R P) : Set P))
    (hxy : (DistribSMul.toLinearMap R P (↑I.den : R) : (a : P) → P) x = y),
    ∃ (a : ↥(↑I : Submodule R P)),
      (LinearMap.restrict (DistribSMul.toLinearMap R P I.den) ⋯ :
            (a : ↥(↑I : Submodule R P)) → ↥(Submodule.map (Algebra.linearMap R P) I.num))
          a =
        Subtype.mk (p := fun (x : P) ↦
          Membership.mem (γ := Submodule R P) (Submodule.map (Algebra.linearMap R P) I.num) x) y hy_1
⊢ ∃ (a : ↥(↑I : Submodule R P)),
    (LinearMap.restrict (DistribSMul.toLinearMap R P I.den) ⋯ :
          (a : ↥(↑I : Submodule R P)) → ↥(Submodule.map (Algebra.linearMap R P) I.num))
        a =
      Subtype.mk (p := fun (x : P) ↦
        Membership.mem (γ := Submodule R P) (Submodule.map (Algebra.linearMap R P) I.num) x) y hy_1

Tactic:
obtain ⟨x, hx, hxy⟩ := hy
-- 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 : FaithfulSMul R P
I : FractionalIdeal S P
reg : IsSMulRegular P I.den
x_1 : ↥(Submodule.map (Algebra.linearMap R P) I.num)
y : P
hy : Membership.mem (γ := Submodule R P) (Submodule.map (Algebra.linearMap R P) I.num) y
x : P
hx : x ∈ (↑(↑I : Submodule R P) : Set P)
hxy : (DistribSMul.toLinearMap R P (↑I.den : R) : (a : P) → P) x = y
simp_rw :
  Eq (α := P) ((DistribSMul.toLinearMap R P I.den : (a : P) → P) x : P)
    ((DistribSMul.toLinearMap R P (↑I.den : R) : (a : P) → P) x : P)
⊢ (LinearMap.restrict (DistribSMul.toLinearMap R P I.den) ⋯ :
        (a : ↥(↑I : Submodule R P)) → ↥(Submodule.map (Algebra.linearMap R P) I.num))
      (Subtype.mk (p := fun (x : P) ↦ x ∈ (↑I : Submodule R P)) x hx) =
    Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Submodule R P) (Submodule.map (Algebra.linearMap R P) I.num) x)
      y hy

Tactic:
simp_rw [LinearMap.restrict_apply, Subtype.ext_iff, ← hxy]

Premises used: Subtype.ext_iff, LinearMap.restrict_apply
-- 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 : FaithfulSMul R P
I : FractionalIdeal S P
reg : IsSMulRegular P I.den
x_1 : ↥(Submodule.map (Algebra.linearMap R P) I.num)
y : P
hy : Membership.mem (γ := Submodule R P) (Submodule.map (Algebra.linearMap R P) I.num) y
x : P
hx : x ∈ (↑(↑I : Submodule R P) : Set P)
hxy : (DistribSMul.toLinearMap R P (↑I.den : R) : (a : P) → P) x = y
⊢ Eq (α := P) ((DistribSMul.toLinearMap R P I.den : (a : P) → P) x : P)
    ((DistribSMul.toLinearMap R P (↑I.den : R) : (a : P) → P) x : P)

Tactic:
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
inst_3 : FaithfulSMul R P
I : FractionalIdeal S P
reg : IsSMulRegular P I.den
x_1 : ↥(Submodule.map (Algebra.linearMap R P) I.num)
y : P
hy : Membership.mem (γ := Submodule R P) (Submodule.map (Algebra.linearMap R P) I.num) y
x : P
hx : x ∈ (↑(↑I : Submodule R P) : Set P)
hxy : (DistribSMul.toLinearMap R P (↑I.den : R) : (a : P) → P) x = y
⊢ ∃ (a : ↥(↑I : Submodule R P)),
    (LinearMap.restrict (DistribSMul.toLinearMap R P I.den) ⋯ :
          (a : ↥(↑I : Submodule R P)) → ↥(Submodule.map (Algebra.linearMap R P) I.num))
        a =
      Subtype.mk (p := fun (x : P) ↦
        Membership.mem (γ := Submodule R P) (Submodule.map (Algebra.linearMap R P) I.num) x) y hy

Tactic:
exact ⟨⟨x, hx⟩, by simp_rw [LinearMap.restrict_apply, Subtype.ext_iff, ← hxy]; 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
I : FractionalIdeal S P
x : P
⊢ x ∈ (↑I : Submodule R P) ↔ x ∈ I

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.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
I J : FractionalIdeal S P
⊢ (↑I : Submodule R P) = (↑J : Submodule R P) → I = J

Tactic:
Subtype.ext

Premises used: FractionalIdeal, FractionalIdeal.coeToSubmodule, Subtype.ext
-- 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
⊢ I = J ↔ (↑I : Submodule R P) = (↑J : Submodule R P)

Tactic:
Subtype.ext_iff

Premises used: Subtype.ext_iff, FractionalIdeal, FractionalIdeal.coeToSubmodule
-- 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
⊢ (∀ (x : P), x ∈ I ↔ x ∈ J) → I = J

Tactic:
SetLike.ext

Premises used: SetLike.ext
-- 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 : IsDomain R
inst_4 : Module.IsTorsionFree R P
inst_5 : Nontrivial P
I : FractionalIdeal S P
h_nz : (↑I.den : R) ≠ 0
x : ↥I
change :
  (Algebra.linearMap R P : (a : R) → P) (↑((equivNum h_nz : (a : ↥(↑I : Submodule R P)) → ↥I.num) x) : R) =
    I.den • (↑x : P)
⊢ (algebraMap R P : (a : R) → P) (↑((equivNum h_nz : (a : ↥(↑I : Submodule R P)) → ↥I.num) x) : R) = I.den • (↑x : P)

Tactic:
change Algebra.linearMap R P _ = _

Premises used: Algebra.linearMap, 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
p : FractionalIdeal S P
s : Set P
hs : s = (↑p : Set P)
⊢ IsFractional S (↑p : Submodule R P)

Tactic:
p.isFractional

Premises used: FractionalIdeal.isFractional
-- 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
p : FractionalIdeal S P
s : Set P
hs : s = (↑p : Set P)
h : (↑p : Submodule R P).copy s hs = (↑p : Submodule R P)
⊢ IsFractional S ((↑p : Submodule R P).copy s hs)

Tactic:
convert! p.isFractional

Premises used: FractionalIdeal.isFractional
-- 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
p : FractionalIdeal S P
s : Set P
hs : s = (↑p : Set P)
h : ∀ (x : P), x ∈ (↑p : Submodule R P).copy s hs ↔ x ∈ (↑p : Submodule R P)
⊢ (↑p : Submodule R P).copy s hs = (↑p : Submodule R P)

Tactic:
ext