awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FormalGroup.Basic (goal)
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)
have 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)
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.RingTheory.FormalGroup.Basic (goal)
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
⊢ 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)
have 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, sorry⟩) :
    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, sorry⟩)) :
    MvPowerSeries (Fin 3) S)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.FormalGroup.Basic (goal)
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)
⊢ 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)
have 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, sorry⟩) :
    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, sorry⟩)) :
    MvPowerSeries (Fin 3) S)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.FormalGroup.Basic (hypothesis)
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} (α := MvPowerSeries (Fin 3) S)
    (subst (R := S)
      ![subst (R := S) ![X 0, X 1]
          (((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),
        X 2]
      (((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))
    (subst (R := S)
      ![X 0,
        subst (R := S) ![X 1, X 2]
          (((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.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))
have this : ∀ (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
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
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
⊢ I.den • (↑I : Submodule R P) = Submodule.map (Algebra.linearMap R P) I.num
have 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)) sorry) sorry •
    (↑I : Submodule R P) =
  LinearMap.range (Algebra.linearMap R P) ⊓ I.den • (↑I : Submodule R P)
Tactic: rw [den, num, Submodule.map_comap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
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)
have 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)) sorry) sorry •
    (↑I : Submodule R P) ≤
  LinearMap.range (Algebra.linearMap R P)
Tactic: refine (inf_of_le_right ?_).symm
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
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
⊢ LinearEquiv.{u_1, u_1, u_2, u_1} (RingHom.id R) ↥(↑I : Submodule R P) ↥I.num
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
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)
⊢ LinearEquiv.{u_1, u_1, u_2, u_1} (RingHom.id R) ↥(↑I : Submodule R P) ↥I.num
have 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) sorry :
            (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) sorry :
            (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: 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
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
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
⊢ LinearEquiv.{u_1, u_1, u_2, u_1} (RingHom.id R) ↥(↑I : Submodule R P) ↥I.num
have 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) sorry :
          (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: 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
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
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) (γ := Submodule R P) (Submodule.map (Algebra.linearMap R P) I.num)
    ((DistribSMul.toLinearMap R P I.den : (a : P) → P) x : P)
have refine_1 : Membership.mem (α := P) (I.den • (↑I : Submodule R P)) ((DistribSMul.toLinearMap R P I.den : (a : P) → P) x : P)
Tactic: rw [← den_mul_self_eq_num]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (hypothesis)
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
⊢ ∃ (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
have hy₁ : y ∈ I.den • (↑I : Submodule R P)
Tactic: rw [← den_mul_self_eq_num] at hy
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
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)
⊢ ∃ (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
have 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) sorry :
          (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
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
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
⊢ (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
have 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)
Tactic: simp_rw [LinearMap.restrict_apply, Subtype.ext_iff, ← hxy]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
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
⊢ (algebraMap R P : (a : R) → P) (↑((equivNum h_nz : (a : ↥(↑I : Submodule R P)) → ↥I.num) x) : R) = I.den • (↑x : P)
have change : (Algebra.linearMap 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 _ = _
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
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).copy s hs)
have h : (↑p : Submodule R P).copy s hs = (↑p : Submodule R P)
Tactic: convert! p.isFractional
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
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)
⊢ (↑p : Submodule R P).copy s hs = (↑p : Submodule R P)
have h : ∀ (x : P), x ∈ (↑p : Submodule R P).copy s hs ↔ x ∈ (↑p : Submodule R P)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
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)
x : P
⊢ x ∈ (↑p : Submodule R P).copy s hs ↔ x ∈ (↑p : Submodule R P)
have h : x ∈ (↑p : Submodule R P).copy (↑p : Set P) sorry ↔ x ∈ (↑p : Submodule R P)
Tactic: simp only [hs]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
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 : Submodule R P
h : I ≤ 1
⊢ IsFractional S I
have right : ∀ b ∈ I, IsInteger R (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 b)
Tactic: use 1, S.one_mem
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
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 : Submodule R P
h : I ≤ 1
b : P
hb : b ∈ I
⊢ IsInteger R (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 b)
have right : IsInteger R b
Tactic: rw [one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
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 : Submodule R P
h : I ≤ 1
b : P
hb : b ∈ I
⊢ IsInteger R b
have right : ∀ (b' : R) (hb : Membership.mem (α := P) I ((algebraMap R P : (a : R) → P) b' : P)),
  IsInteger.{u_1, u_2} R (S := P) ((algebraMap R P : (a : R) → P) b' : P)
Tactic: obtain ⟨b', b'_mem, rfl⟩ := mem_one.mp (h hb)
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
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 : Submodule R P
J : FractionalIdeal S P
hIJ : I ≤ (↑J : Submodule R P)
⊢ IsFractional S I
have obtain : ∀ (a : R) (a_mem : a ∈ S) (ha : ∀ b ∈ (↑J : Submodule R P), IsInteger R (a • b)), IsFractional S I
Tactic: obtain ⟨a, a_mem, ha⟩ := J.isFractional
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
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 : Submodule R P
J : FractionalIdeal S P
hIJ : I ≤ (↑J : Submodule R P)
a : R
a_mem : a ∈ S
ha : ∀ b ∈ (↑J : Submodule R P), IsInteger R (a • b)
⊢ IsFractional S I
have right : ∀ b ∈ I, IsInteger R (a • b)
Tactic: use a, a_mem
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (hypothesis)
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 : P
h : Membership.mem (γ := FractionalIdeal S P) 0 x
x' : R
x'_mem_zero : x' ∈ (↑0 : Set R)
x'_eq_x : (Algebra.linearMap R P : (a : R) → P) x' = x
⊢ x = 0
have x'_eq_zero : x' = 0
Tactic: have x'_eq_zero : x' = 0 := x'_mem_zero
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
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
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
⊢ I = 0
have rw : (↑I : Submodule R P) ≤ ⊥
Tactic: rw [← coeToSubmodule_eq_bot, eq_bot_iff]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
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
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
x : P
hx : x ∈ (↑I : Submodule R P)
⊢ Membership.mem (γ := Submodule R P) ⊥ x
have suffices : (↑I.den : R) • x = 0
Tactic: suffices (den I : R) • x = 0 from
    (smul_eq_zero.mp this).resolve_left (ne_of_mem_of_not_mem (SetLike.coe_mem _) hS)
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
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
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
x : P
hx : x ∈ (↑I : Submodule R P)
⊢ I.den • (↑I : Submodule R P) = ⊥
have rw : Eq (α := Submodule R P) (Submodule.map (Algebra.linearMap R P) I.num) ⊥
Tactic: rw [den_mul_self_eq_num, hI, Submodule.map_bot]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
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
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
x : P
hx : x ∈ (↑I : Submodule R P)
rw : Eq (α := Submodule R P) (Submodule.map (Algebra.linearMap R P) I.num) ⊥
⊢ I.den • (↑I : Submodule R P) = ⊥
have rw₁ : Eq (α := Submodule R P) (Submodule.map (Algebra.linearMap R P) ⊥) ⊥
Tactic: rw [den_mul_self_eq_num, hI, Submodule.map_bot]