awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst_7 : Fact (Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑i : (a : M) → N))
h : Baer R Q
y : N
r : R
a : ↥(supExtensionOfMaxSingleton i f y)
eq1 : r • (↑a : N) = (↑(r • ExtensionOfMaxAdjoin.fst i a) : N) + (r • ExtensionOfMaxAdjoin.snd i a) • y
⊢ ExtensionOfMaxAdjoin.extensionToFun i f h (r • a) = r • ExtensionOfMaxAdjoin.extensionToFun i f h a
have rw : r •
    HAdd.hAdd (β := Q)
      ((↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) (ExtensionOfMaxAdjoin.fst i a))
      ((ExtensionOfMaxAdjoin.extendIdealTo i f h y : (a : R) → Q) (ExtensionOfMaxAdjoin.snd i a) : Q) =
  r • ExtensionOfMaxAdjoin.extensionToFun i f h a
Tactic: rw [ExtensionOfMaxAdjoin.extensionToFun_wd i f h (r • a :) _ _ eq1, map_smul,
          LinearPMap.map_smul, ← smul_add]
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst_7 : Fact (Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑i : (a : M) → N))
h : Baer R Q
y : N
m : M
⊢ (f : (a : M) → Q) m =
    (↑{ domain := supExtensionOfMaxSingleton i f y,
            toFun :=
              { toFun := ExtensionOfMaxAdjoin.extensionToFun i f h, map_add' := ⋯, map_smul' := ⋯ :
                LinearMap.{u, u, u_2, v} (RingHom.id R) (↥(supExtensionOfMaxSingleton i f y)) Q } :
            N →ₗ.[R] Q } :
        ↥{ domain := supExtensionOfMaxSingleton i f y,
                toFun :=
                  { toFun := ExtensionOfMaxAdjoin.extensionToFun i f h, map_add' := ⋯, map_smul' := ⋯ } }.domain →
          Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ supExtensionOfMaxSingleton i f y) ((i : (a : M) → N) m) ⋯)
have dsimp : (f : (a : M) → Q) m =
  ExtensionOfMaxAdjoin.extensionToFun i f h (y := y)
    (Subtype.mk (p := fun (x : N) ↦ x ∈ supExtensionOfMaxSingleton i f y) ((i : (a : M) → N) m) sorry)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst_7 : Fact (Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑i : (a : M) → N))
h : Baer R Q
y : N
m : M
⊢ (f : (a : M) → Q) m =
    ExtensionOfMaxAdjoin.extensionToFun i f h (y := y)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ supExtensionOfMaxSingleton i f y) ((i : (a : M) → N) m) ⋯)
have rw : (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ supExtensionOfMaxSingleton i f y) ((i : (a : M) → N) m) sorry) : N) =
  HAdd.hAdd (α := N)
    ((↑(Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((i : (a : M) → N) m) sorry) : N) : N)
    (HSMul.hSMul.{u, u_2, u_2} (α := R) 0 y)
Tactic: rw [(extensionOfMax i f).is_extension,
      ExtensionOfMaxAdjoin.extensionToFun_wd i f h _ ⟨i m, _⟩ 0 _, map_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst_7 : Fact (Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑i : (a : M) → N))
h : Baer R Q
y : N
x : ↥(extensionOfMax i f).domain
x' : ↥(extensionOfMaxAdjoin i f h y).domain
EQ : (↑x : N) = (↑x' : N)
⊢ (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x =
    (↑(extensionOfMaxAdjoin i f h y).toLinearPMap : ↥(extensionOfMaxAdjoin i f h y).domain → Q) x'
have symm : (↑(extensionOfMaxAdjoin i f h y).toLinearPMap : ↥(extensionOfMaxAdjoin i f h y).domain → Q) x' =
  (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst_7 : Fact (Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑i : (a : M) → N))
h : Baer R Q
y : N
x : ↥(extensionOfMax i f).domain
x' : ↥(extensionOfMaxAdjoin i f h y).domain
EQ : (↑x : N) = (↑x' : N)
⊢ (↑(extensionOfMaxAdjoin i f h y).toLinearPMap : ↥(extensionOfMaxAdjoin i f h y).domain → Q) x' =
    (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x
have change : ExtensionOfMaxAdjoin.extensionToFun i f h x' = (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x
Tactic: change ExtensionOfMaxAdjoin.extensionToFun i f h _ = _
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst_7 : Fact (Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑i : (a : M) → N))
h : Baer R Q
y : N
x : ↥(extensionOfMax i f).domain
x' : ↥(extensionOfMaxAdjoin i f h y).domain
EQ : (↑x : N) = (↑x' : N)
⊢ ExtensionOfMaxAdjoin.extensionToFun i f h x' =
    (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x
have rw : HAdd.hAdd (β := Q) ((↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x)
    ((ExtensionOfMaxAdjoin.extendIdealTo i f h y : (a : R) → Q) 0 : Q) =
  (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x
Tactic: rw [ExtensionOfMaxAdjoin.extensionToFun_wd i f h x' x 0 (by simp [EQ]), map_zero,
      add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst_7 : Fact (Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑i : (a : M) → N))
h : Baer R Q
y : N
x : ↥(extensionOfMax i f).domain
x' : ↥(extensionOfMaxAdjoin i f h y).domain
EQ : (↑x : N) = (↑x' : N)
rw :
  HAdd.hAdd (β := Q) ((↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x)
      ((ExtensionOfMaxAdjoin.extendIdealTo i f h y : (a : R) → Q) 0 : Q) =
    (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x
⊢ ExtensionOfMaxAdjoin.extensionToFun i f h x' =
    (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x
have rw₁ : (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x + 0 =
  (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x
Tactic: rw [ExtensionOfMaxAdjoin.extensionToFun_wd i f h x' x 0 (by simp [EQ]), map_zero,
      add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst_7 : Fact (Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑i : (a : M) → N))
h : Baer R Q
y : N
x : ↥(extensionOfMax i f).domain
x' : ↥(extensionOfMaxAdjoin i f h y).domain
EQ : (↑x : N) = (↑x' : N)
rw :
  HAdd.hAdd (β := Q) ((↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x)
      ((ExtensionOfMaxAdjoin.extendIdealTo i f h y : (a : R) → Q) 0 : Q) =
    (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x
rw₁ :
  (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x + 0 =
    (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x
⊢ ExtensionOfMaxAdjoin.extensionToFun i f h x' =
    (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x
have rw₂ : (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x =
  (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x
Tactic: rw [ExtensionOfMaxAdjoin.extensionToFun_wd i f h x' x 0 (by simp [EQ]), map_zero,
      add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst_7 : Fact (Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑i : (a : M) → N))
h : Baer R Q
⊢ (extensionOfMax i f).domain = ⊤
have refine : ∀ (y : N), y ∈ (extensionOfMax i f).domain
Tactic: refine Submodule.eq_top_iff'.mpr fun y => ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst_7 : Fact (Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑i : (a : M) → N))
h : Baer R Q
y : N
⊢ y ∈ (extensionOfMax i f).domain
have rw : ∃ y_1 ∈ (extensionOfMax i f).domain, ∃ (z : N), Membership.mem (γ := Submodule R N) (R ∙ y) z ∧ y_1 + z = y
Tactic: rw [← extensionOfMax_is_max i f _ (extensionOfMax_le i f h), extensionOfMaxAdjoin,
    Submodule.mem_sup]
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
h : Baer R Q
f : M →ₗ[R] N
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
g : M →ₗ[R] Q
this : Fact (Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N))
x y : N
⊢ (↑(extensionOfMax f g).toLinearPMap : ↥(extensionOfMax f g).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax f g).domain) (x + y) ⋯) =
    (↑(extensionOfMax f g).toLinearPMap : ↥(extensionOfMax f g).domain → Q)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax f g).domain) x ⋯) +
      (↑(extensionOfMax f g).toLinearPMap : ↥(extensionOfMax f g).domain → Q)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax f g).domain) y ⋯)
have rw : (↑(extensionOfMax f g).toLinearPMap : ↥(extensionOfMax f g).domain → Q)
    (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax f g).domain) (x + y) sorry) =
  (↑(extensionOfMax f g).toLinearPMap : ↥(extensionOfMax f g).domain → Q)
    (HAdd.hAdd (α := ↥(extensionOfMax f g).domain) (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax f g).domain) x sorry)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax f g).domain) y sorry))
Tactic: rw [← LinearPMap.map_add]
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
h : Baer R Q
f : M →ₗ[R] N
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
g : M →ₗ[R] Q
this : Fact (Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N))
r : R
x : N
⊢ (↑(extensionOfMax f g).toLinearPMap : ↥(extensionOfMax f g).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax f g).domain) (r • x) ⋯) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
      ((↑(extensionOfMax f g).toLinearPMap : ↥(extensionOfMax f g).domain → Q)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax f g).domain) x ⋯))
have rw : (↑(extensionOfMax f g).toLinearPMap : ↥(extensionOfMax f g).domain → Q)
    (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax f g).domain) (r • x) sorry) =
  (↑(extensionOfMax f g).toLinearPMap : ↥(extensionOfMax f g).domain → Q)
    (HSMul.hSMul (α := R) (β := ↥(extensionOfMax f g).domain) ((RingHom.id R : (a : R) → R) r : R)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax f g).domain) x sorry))
Tactic: rw [← LinearPMap.map_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
h : Baer R Q
X Y : Type v
x : AddCommGroup X
x_1 : AddCommGroup Y
x_2 : Module R X
x_3 : Module R Y
i : X →ₗ[R] Y
hi : Function.Injective (α := X) (β := Y) (⇑i : (a : X) → Y)
f : X →ₗ[R] Q
⊢ ∃ (h : Y →ₗ[R] Q),
    ∀ (x_4 : X), Eq (α := Q) ((h : (a : Y) → Q) ((i : (a : X) → Y) x_4 : Y) : Q) ((f : (a : X) → Q) x_4 : Q)
have obtain : ∀ (h : Y →ₗ[R] Q) (H : h ∘ₗ i = f),
  ∃ (h : Y →ₗ[R] Q),
    ∀ (x_4 : X), Eq (α := Q) ((h : (a : Y) → Q) ((i : (a : X) → Y) x_4 : Y) : Q) ((f : (a : X) → Q) x_4 : Q)
Tactic: obtain ⟨h, H⟩ := Module.Baer.extension_property h i hi f
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
inst_3 : Small.{v, u} R
inj : Injective R Q
I : Ideal R
g : ↥I →ₗ[R] Q
eI : LinearEquiv.{u, u, v, u} (RingHom.id R) (Shrink.{v, u} ↥I) ↥I := Shrink.linearEquiv R ↥I
eR : LinearEquiv.{u, u, v, u} (RingHom.id R) (Shrink.{v, u} R) R := Shrink.linearEquiv R R
⊢ ∃ (g' : R →ₗ[R] Q),
    ∀ (x : R) (mem : x ∈ I),
      Eq.{v + 1} (α := Q) ((g' : (a : R) → Q) x : Q)
        ((g : (a : ↥I) → Q) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : Q)
have obtain : ∀ (g' : Shrink.{v, u} R →ₗ[R] Q)
  (hg' :
    ∀ (x : Shrink.{v, u} ↥I),
      Eq (α := Q)
        ((g' : (a : Shrink.{v, u} R) → Q)
            (((↑eR.symm : R →ₗ[R] Shrink.{v, u} R) ∘ₗ Submodule.subtype I ∘ₗ (↑eI : Shrink.{v, u} ↥I →ₗ[R] ↥I) :
                  (a : Shrink.{v, u} ↥I) → Shrink.{v, u} R)
                x :
              Shrink.{v, u} R) :
          Q)
        ((g ∘ₗ (↑eI : Shrink.{v, u} ↥I →ₗ[R] ↥I) : (a : Shrink.{v, u} ↥I) → Q) x : Q)),
  ∃ (g' : R →ₗ[R] Q),
    ∀ (x : R) (mem : x ∈ I),
      Eq.{v + 1} (α := Q) ((g' : (a : R) → Q) x : Q)
        ((g : (a : ↥I) → Q) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : Q)
Tactic: obtain ⟨g', hg'⟩ := Module.Injective.out (eR.symm.toLinearMap ∘ₗ I.subtype ∘ₗ eI.toLinearMap)
    (eR.symm.injective.comp <| Subtype.val_injective.comp eI.injective) (g ∘ₗ eI.toLinearMap)
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R_1 : Type u
inst : Ring R_1
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R_1 Q
R : Type u
inst_3 : Ring R
ι : Type w
M : ι → Type v
inst_4 : Small.{v, u} R
inst_5 : (i : ι) → AddCommGroup (M i)
inst_6 : (i : ι) → Module.{u, v} R (M i)
inst_7 : ∀ (i : ι), Injective.{u, v} R (M i)
X Y : Type (max v w)
x : AddCommGroup X
x_1 : AddCommGroup Y
x_2 : Module R X
x_3 : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective (α := X) (β := Y) (⇑f : (a : X) → Y)
g : X →ₗ[R] (i : ι) → M i
⊢ ∃ (h : Y →ₗ[R] (i : ι) → M i),
    ∀ (x_4 : X),
      Eq (α := (i : ι) → M i) ((h : (a : Y) → (i : ι) → M i) ((f : (a : X) → Y) x_4 : Y) : (i : ι) → M i)
        ((g : (a : X) → (i : ι) → M i) x_4 : (i : ι) → M i)
have choose : ∀ (l : (i : ι) → Y →ₗ[R] M i) (hl : ∀ (i : ι), l i ∘ₗ f = LinearMap.proj (φ := M) i ∘ₗ g),
  ∃ (h : Y →ₗ[R] (i : ι) → M i),
    ∀ (x_4 : X),
      Eq (α := (i : ι) → M i) ((h : (a : Y) → (i : ι) → M i) ((f : (a : X) → Y) x_4 : Y) : (i : ι) → M i)
        ((g : (a : X) → (i : ι) → M i) x_4 : (i : ι) → M i)
Tactic: choose l hl using fun i ↦ extension_property R _ _ _ f hf ((LinearMap.proj i).comp g)
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R_1 : Type u
inst : Ring R_1
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R_1 Q
R : Type u
inst_3 : Ring R
ι : Type w
M : ι → Type v
inst_4 : Small.{v, u} R
inst_5 : (i : ι) → AddCommGroup (M i)
inst_6 : (i : ι) → Module.{u, v} R (M i)
inst_7 : ∀ (i : ι), Injective.{u, v} R (M i)
X Y : Type (max v w)
x : AddCommGroup X
x_1 : AddCommGroup Y
x_2 : Module R X
x_3 : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective (α := X) (β := Y) (⇑f : (a : X) → Y)
g : X →ₗ[R] (i : ι) → M i
l : (i : ι) → Y →ₗ[R] M i
hl : ∀ (i : ι), l i ∘ₗ f = LinearMap.proj (φ := M) i ∘ₗ g
⊢ ∃ (h : Y →ₗ[R] (i : ι) → M i),
    ∀ (x_4 : X),
      Eq (α := (i : ι) → M i) ((h : (a : Y) → (i : ι) → M i) ((f : (a : X) → Y) x_4 : Y) : (i : ι) → M i)
        ((g : (a : X) → (i : ι) → M i) x_4 : (i : ι) → M i)
have refine : ∀ (x_4 : X),
  Eq (α := (i : ι) → M i)
    ((LinearMap.pi (φ := M) l : (a : Y) → (i : ι) → M i) ((f : (a : X) → Y) x_4 : Y) : (i : ι) → M i)
    ((g : (a : X) → (i : ι) → M i) x_4 : (i : ι) → M i)
Tactic: refine ⟨LinearMap.pi l, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R_1 : Type u
inst : Ring R_1
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R_1 Q
R : Type u
inst_3 : Ring R
ι : Type w
M : ι → Type v
inst_4 : Small.{v, u} R
inst_5 : (i : ι) → AddCommGroup (M i)
inst_6 : (i : ι) → Module.{u, v} R (M i)
inst_7 : ∀ (i : ι), Injective.{u, v} R (M i)
X Y : Type (max v w)
x_1 : AddCommGroup X
x_2 : AddCommGroup Y
x_3 : Module R X
x_4 : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective (α := X) (β := Y) (⇑f : (a : X) → Y)
g : X →ₗ[R] (i : ι) → M i
l : (i : ι) → Y →ₗ[R] M i
hl : ∀ (i : ι), l i ∘ₗ f = LinearMap.proj (φ := M) i ∘ₗ g
x : X
⊢ Eq (α := (i : ι) → M i)
    ((LinearMap.pi (φ := M) l : (a : Y) → (i : ι) → M i) ((f : (a : X) → Y) x : Y) : (i : ι) → M i)
    ((g : (a : X) → (i : ι) → M i) x : (i : ι) → M i)
have h : ∀ (i : ι),
  Eq.{v + 1} (α := M i) ((LinearMap.pi (φ := M) l : (a : Y) → (i : ι) → M i) ((f : (a : X) → Y) x : Y) i : M i)
    ((g : (a : X) → (i : ι) → M i) x i : M i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : Small.{v, u} R
S : Type u'
inst_2 : Ring S
M : Type v
N : Type v'
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[(↑e₁ : R →+* S)] N
inj : Injective R M
⊢ Injective S N
have apply : ∀ (I : Ideal S) (g : ↥I →ₗ[S] N),
  ∃ (g' : S →ₗ[S] N),
    ∀ (x : S) (mem : x ∈ I),
      Eq.{v' + 1} (α := N) ((g' : (a : S) → N) x : N)
        ((g : (a : ↥I) → N) (Subtype.mk (p := fun (x : S) ↦ x ∈ I) x mem) : N)
Tactic: apply Module.Baer.injective (fun I g ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (hypothesis)
Goal:
R : Type u
inst : Ring R
inst_1 : Small.{v, u} R
S : Type u'
inst_2 : Ring S
M : Type v
N : Type v'
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[(↑e₁ : R →+* S)] N
inj : Injective R M
I : Ideal S
g : ↥I →ₗ[S] N
I' : Submodule R R := Submodule.map (↑e₁.symm.toSemilinearEquiv : S →ₛₗ[(↑e₁.symm : S →+* R)] R) I
e : ↥I' ≃ₛₗ[(↑e₁ : R →+* S)] ↥I := (e₁.symm.toSemilinearEquiv.submoduleMap I).symm
f : ↥I' →ₗ[R] M := (↑e₂.symm : N →ₛₗ[(↑e₁.symm : S →+* R)] M) ∘ₛₗ g ∘ₛₗ (↑e : ↥I' →ₛₗ[(↑e₁ : R →+* S)] ↥I)
⊢ ∃ (g' : S →ₗ[S] N),
    ∀ (x : S) (mem : x ∈ I),
      Eq.{v' + 1} (α := N) ((g' : (a : S) → N) x : N)
        ((g : (a : ↥I) → N) (Subtype.mk (p := fun (x : S) ↦ x ∈ I) x mem) : N)
have hf : ∀ (x : R) (hx : x ∈ I'),
  Eq.{v + 1} (α := M) ((f : (a : ↥I') → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I') x hx) : M)
    ((e₂.symm : (a : N) → M)
        ((g : (a : ↥I) → N) (Subtype.mk (p := fun (x : S) ↦ x ∈ I) ((e₁ : (a : R) → S) x) sorry : ↥I) : N) :
      M)
Tactic: have hf (x) (hx : x ∈ I') : f ⟨x, hx⟩ = e₂.symm (g ⟨e₁ x, by simp_all [I']⟩) := rfl
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : Small.{v, u} R
S : Type u'
inst_2 : Ring S
M : Type v
N : Type v'
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[(↑e₁ : R →+* S)] N
inj : Injective R M
I : Ideal S
g : ↥I →ₗ[S] N
I' : Submodule R R := Submodule.map (↑e₁.symm.toSemilinearEquiv : S →ₛₗ[(↑e₁.symm : S →+* R)] R) I
e : ↥I' ≃ₛₗ[(↑e₁ : R →+* S)] ↥I := (e₁.symm.toSemilinearEquiv.submoduleMap I).symm
f : ↥I' →ₗ[R] M := (↑e₂.symm : N →ₛₗ[(↑e₁.symm : S →+* R)] M) ∘ₛₗ g ∘ₛₗ (↑e : ↥I' →ₛₗ[(↑e₁ : R →+* S)] ↥I)
hf :
  ∀ (x : R) (hx : x ∈ I'),
    Eq.{v + 1} (α := M) ((f : (a : ↥I') → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I') x hx) : M)
      ((e₂.symm : (a : N) → M)
          ((g : (a : ↥I) → N) (Subtype.mk (p := fun (x : S) ↦ x ∈ I) ((e₁ : (a : R) → S) x) ⋯ : ↥I) : N) :
        M)
⊢ ∃ (g' : S →ₗ[S] N),
    ∀ (x : S) (mem : x ∈ I),
      Eq.{v' + 1} (α := N) ((g' : (a : S) → N) x : N)
        ((g : (a : ↥I) → N) (Subtype.mk (p := fun (x : S) ↦ x ∈ I) x mem) : N)
have obtain : ∀ (f' : R →ₗ[R] M)
  (hf' :
    ∀ (x : R) (mem : x ∈ I'),
      Eq.{v + 1} (α := M) ((f' : (a : R) → M) x : M)
        ((f : (a : ↥I') → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I') x mem) : M)),
  ∃ (g' : S →ₗ[S] N),
    ∀ (x : S) (mem : x ∈ I),
      Eq.{v' + 1} (α := N) ((g' : (a : S) → N) x : N)
        ((g : (a : ↥I) → N) (Subtype.mk (p := fun (x : S) ↦ x ∈ I) x mem) : N)
Tactic: obtain ⟨f', hf'⟩ := Module.Baer.of_injective ‹_› I' f
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
M : Submodule R V
inst_7 : IsLattice A M
⊢ Module.Finite.{u_1, u_3} R ↥M
have rw : M.FG
Tactic: rw [Module.Finite.iff_fg]
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
M : Submodule R V
inst_7 : IsLattice A M
a : Aˣ
⊢ (a • M).FG
have obtain : ∀ (s : Finset V) [IsLattice A (span R (↑s : Set V))], (HSMul.hSMul (β := Submodule R V) a (span R (↑s : Set V))).FG
Tactic: obtain ⟨s, rfl⟩ := IsLattice.fg (M := M)
Cleared hypotheses: M, inst_7
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
a : Aˣ
s : Finset V
inst_7 : IsLattice A (span R (↑s : Set V))
⊢ (HSMul.hSMul (β := Submodule R V) a (span R (↑s : Set V))).FG
have rw : FG (span R (a • (↑s : Set V)))
Tactic: rw [Submodule.smul_span]
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
a : Aˣ
s : Finset V
inst_7 : IsLattice A (span R (↑s : Set V))
⊢ FG (span R (a • (↑s : Set V)))
have this : Finite.{u_3 + 1} (↑(a • (↑s : Set V)) : Type u_3)
Tactic: have : Finite (a • (s : Set V) : Set V) := Finite.Set.finite_image _ _
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
M : Submodule R V
inst_7 : IsLattice A M
a : Aˣ
⊢ Eq (α := Submodule A V) (span A (↑(a • M) : Set V)) ⊤
have rw : HSMul.hSMul (β := Submodule A V) a ⊤ = ⊤
Tactic: rw [Submodule.coe_pointwise_smul, ← Submodule.smul_span, IsLattice.span_eq_top]
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
M : Submodule R V
inst_7 : IsLattice A M
a : Aˣ
⊢ HSMul.hSMul (β := Submodule A V) a ⊤ = ⊤
have h : ∀ (x : V), x ∈ HSMul.hSMul (β := Submodule A V) a ⊤ ↔ Membership.mem (γ := Submodule A V) ⊤ x
Tactic: ext x