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))
m : M
⊢ Eq.{v + 1} (α := Q) ((f : (a : M) → Q) m : Q)
    ((↑{ domain := i.range,
              toFun :=
                {
                  toFun := fun (x : ↥i.range) ↦
                    (f : (a : M) → Q) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) ⋯),
                  map_add' := ⋯, map_smul' := ⋯ } } :
          ↥{ domain := i.range,
                  toFun :=
                    { toFun := fun (x : ↥i.range) ↦ (f : (a : M) → Q) (Exists.choose ⋯), map_add' := ⋯,
                      map_smul' := ⋯ } }.domain →
            Q)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ i.range) ((i : (a : M) → N) m) ⋯) :
      Q)
have simp : Eq.{v + 1} (α := Q) ((f : (a : M) → Q) m : Q)
  (({
          toFun := fun (x : ↥i.range) ↦
            (f : (a : M) → Q) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) sorry),
          map_add' := sorry } :
        (a : ↥i.range) → Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ i.range) ((i : (a : M) → N) m) sorry : ↥i.range) :
    Q)
Tactic: simp only [LinearPMap.mk_apply, LinearMap.coe_mk]
-- 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))
m : M
⊢ Eq.{v + 1} (α := Q) ((f : (a : M) → Q) m : Q)
    (({
            toFun := fun (x : ↥i.range) ↦
              (f : (a : M) → Q) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) ⋯),
            map_add' := ⋯ } :
          (a : ↥i.range) → Q)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ i.range) ((i : (a : M) → N) m) ⋯ : ↥i.range) :
      Q)
have dsimp : Eq.{v + 1} (α := Q) ((f : (a : M) → Q) m : Q)
  ((f : (a : M) → Q)
      (Exists.choose (p := fun (y : M) ↦ Eq.{u_2 + 1} (α := N) ((i : (a : M) → N) y : N) ((i : (a : M) → N) m : N)) sorry) :
    Q)
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))
m : M
⊢ Eq.{v + 1} (α := Q) ((f : (a : M) → Q) m : Q)
    ((f : (a : M) → Q)
        (Exists.choose (p := fun (y : M) ↦ Eq.{u_2 + 1} (α := N) ((i : (a : M) → N) y : N) ((i : (a : M) → N) m : N))
          ⋯) :
      Q)
have h : m = Exists.choose (p := fun (y : M) ↦ Eq.{u_2 + 1} (α := N) ((i : (a : M) → N) y : N) ((i : (a : M) → N) m : N)) sorry
Tactic: apply congrArg
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (hypothesis)
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))
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
⊢ ∃ (a : ↥(extensionOfMax i f).domain) (b : R), (↑x : N) = (↑a : N) + b • y
have mem1 : (↑x : N) ∈ (↑(supExtensionOfMaxSingleton i f y) : Set N)
Tactic: have mem1 : x.1 ∈ (_ : Set _) := x.2
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (hypothesis)
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))
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
mem1 : (↑x : N) ∈ (↑(supExtensionOfMaxSingleton i f y) : Set N)
⊢ ∃ (a : ↥(extensionOfMax i f).domain) (b : R), (↑x : N) = (↑a : N) + b • y
have mem1₁ : (↑x : N) ∈ (↑(extensionOfMax i f).domain : Set N) + (↑(R ∙ y) : Set N)
Tactic: rw [Submodule.coe_sup] at mem1
Cleared hypotheses: mem1
-- 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))
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
mem1 : (↑x : N) ∈ (↑(extensionOfMax i f).domain : Set N) + (↑(R ∙ y) : Set N)
⊢ ∃ (a : ↥(extensionOfMax i f).domain) (b : R), (↑x : N) = (↑a : N) + b • y
have rcases : ∀ (a : N) (a_mem : a ∈ (↑(extensionOfMax i f).domain : Set N)) (b : N)
  (b_mem : Membership.mem (γ := Submodule R N) (R ∙ y) b) (eq1 : (fun (x1 x2 : N) ↦ x1 + x2) a b = (↑x : N)),
  ∃ (a : ↥(extensionOfMax i f).domain) (b : R), (↑x : N) = (↑a : N) + b • y
Tactic: rcases mem1 with ⟨a, a_mem, b, b_mem : b ∈ (Submodule.span R _ : Submodule R N), eq1⟩
Cleared hypotheses: mem1
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (hypothesis)
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))
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
a : N
a_mem : a ∈ (↑(extensionOfMax i f).domain : Set N)
b : N
b_mem : Membership.mem (γ := Submodule R N) (R ∙ y) b
eq1 : (fun (x1 x2 : N) ↦ x1 + x2) a b = (↑x : N)
⊢ ∃ (a : ↥(extensionOfMax i f).domain) (b : R), (↑x : N) = (↑a : N) + b • y
have b_mem₁ : ∃ (a : R), a • y = b
Tactic: rw [Submodule.mem_span_singleton] at b_mem
Cleared hypotheses: b_mem, eq1
-- 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))
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
a : N
a_mem : a ∈ (↑(extensionOfMax i f).domain : Set N)
b : N
b_mem : ∃ (a : R), a • y = b
eq1 : (fun (x1 x2 : N) ↦ x1 + x2) a b = (↑x : N)
⊢ ∃ (a : ↥(extensionOfMax i f).domain) (b : R), (↑x : N) = (↑a : N) + b • y
have rcases : ∀ (z : R) (eq2 : z • y = b), ∃ (a : ↥(extensionOfMax i f).domain) (b : R), (↑x : N) = (↑a : N) + b • y
Tactic: rcases b_mem with ⟨z, eq2⟩
Cleared hypotheses: b_mem
-- 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))
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
a : N
a_mem : a ∈ (↑(extensionOfMax i f).domain : Set N)
b : N
eq1 : (fun (x1 x2 : N) ↦ x1 + x2) a b = (↑x : N)
z : R
eq2 : z • y = b
⊢ (↑x : N) = (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) a a_mem) : N) + z • y
have rw : (fun (x1 x2 : N) ↦ x1 + x2) a b =
  (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) a a_mem) : N) + z • y
Tactic: rw [← eq1, ← eq2]
-- 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))
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
a : N
a_mem : a ∈ (↑(extensionOfMax i f).domain : Set N)
b : N
eq1 : (fun (x1 x2 : N) ↦ x1 + x2) a b = (↑x : N)
z : R
eq2 : z • y = b
rw :
  (fun (x1 x2 : N) ↦ x1 + x2) a b =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) a a_mem) : N) + z • y
⊢ (↑x : N) = (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) a a_mem) : N) + z • y
have rw₁ : (fun (x1 x2 : N) ↦ x1 + x2) a (z • y) =
  (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) a a_mem) : N) + z • y
Tactic: rw [← eq1, ← eq2]
-- 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))
y : N
z1 z2 : ↥(ideal i f y)
⊢ (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((↑(z1 + z2) : R) • y) ⋯) =
    (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((↑z1 : R) • y) ⋯) +
      (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((↑z2 : R) • y) ⋯)
have simp_rw : (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
    (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((↑(z1 + z2) : R) • y) sorry) =
  (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
    (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((↑z1 : R) • y) sorry +
      Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((↑z2 : R) • y) sorry)
Tactic: simp_rw [← (extensionOfMax i f).toLinearPMap.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
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))
y : N
z1 z2 : ↥(ideal i f y)
⊢ (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((↑(z1 + z2) : R) • y) ⋯) =
    (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((↑z1 : R) • y) ⋯ +
        Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((↑z2 : R) • y) ⋯)
have e_a : (↑(z1 + z2) : R) • y =
  (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((↑z1 : R) • y) sorry) : N) +
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((↑z2 : R) • y) sorry) : N)
Tactic: congr
-- 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))
y : N
z1 : R
z2 : ↥(ideal i f y)
⊢ (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((↑(z1 • z2) : R) • y) ⋯) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) z1 : R)
      ((↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((↑z2 : R) • y) ⋯))
have simp_rw : (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
    (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((↑(z1 • z2) : R) • y) sorry) =
  (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
    (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) z1 : R)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((↑z2 : R) • y) sorry))
Tactic: simp_rw [← (extensionOfMax i f).toLinearPMap.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
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))
y : N
z1 : R
z2 : ↥(ideal i f y)
⊢ (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((↑(z1 • z2) : R) • y) ⋯) =
    (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
      (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) z1 : R)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((↑z2 : R) • y) ⋯))
have e_a : (↑(z1 • z2) : R) • y =
  HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) z1 : R)
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((↑z2 : R) • y) sorry) : N)
Tactic: congr 2
-- 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
eq1 : r • y = 0
⊢ r ∈ ideal i f y
have change : r • y ∈ (extensionOfMax i f).domain
Tactic: change (r • y) ∈ (extensionOfMax i f).toLinearPMap.domain
-- 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
eq1 : r • y = 0
⊢ r • y ∈ (extensionOfMax i f).domain
have rw : 0 ∈ (extensionOfMax i f).domain
Tactic: rw [eq1]
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (hypothesis)
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
eq1 : r • y = 0
⊢ Eq.{v + 1} (α := Q) ((extendIdealTo i f h y : (a : R) → Q) r : Q) (0 : Q)
have this : r ∈ ideal i f y
Tactic: have : r ∈ ideal i f y := by
    change (r • y) ∈ (extensionOfMax i f).toLinearPMap.domain
    rw [eq1]
    apply Submodule.zero_mem _
-- 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
eq1 : r • y = 0
this : r ∈ ideal i f y
⊢ Eq.{v + 1} (α := Q) ((extendIdealTo i f h y : (a : R) → Q) r : Q) (0 : Q)
have rw : Eq.{v + 1} (α := Q)
  ((idealTo i f y : (a : ↥(ideal i f y)) → Q) (Subtype.mk (p := fun (x : R) ↦ x ∈ ideal i f y) r this) : Q) (0 : Q)
Tactic: rw [ExtensionOfMaxAdjoin.extendIdealTo_is_extension i f h y r this]
-- 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
eq1 : r • y = 0
this : r ∈ ideal i f y
⊢ Eq.{v + 1} (α := Q)
    ((idealTo i f y : (a : ↥(ideal i f y)) → Q) (Subtype.mk (p := fun (x : R) ↦ x ∈ ideal i f y) r this) : Q) (0 : Q)
have dsimp : (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
    (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) (r • y) sorry) =
  0
Tactic: dsimp [ExtensionOfMaxAdjoin.idealTo]
-- 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' : R
eq1 : r • y = r' • y
⊢ Eq.{v + 1} (α := Q) ((extendIdealTo i f h y : (a : R) → Q) r : Q) ((extendIdealTo i f h y : (a : R) → Q) r' : Q)
have rw : Eq.{v + 1} (α := Q) ((extendIdealTo i f h y : (a : R) → Q) (r - r') : Q) (0 : Q)
Tactic: rw [← sub_eq_zero, ← map_sub]
-- 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' : R
eq1 : r • y = r' • y
⊢ Eq.{v + 1} (α := Q) ((extendIdealTo i f h y : (a : R) → Q) (r - r') : Q) (0 : Q)
have convert_2 : (r - r') • y = 0
Tactic: convert! ExtensionOfMaxAdjoin.extendIdealTo_wd' i f h (r - r') _
-- 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' : R
eq1 : r • y = r' • y
⊢ (r - r') • y = 0
have convert_2 : r • y - r' • y = 0
Tactic: rw [sub_smul, sub_eq_zero, eq1]
-- 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' : R
eq1 : r • y = r' • y
convert_2 : r • y - r' • y = 0
convert_2₁ : r • y = r' • y
⊢ (r - r') • y = 0
have convert_2₂ : r' • y = r' • y
Tactic: rw [sub_smul, sub_eq_zero, eq1]
-- 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 : ↥(supExtensionOfMaxSingleton i f y)
a : ↥(extensionOfMax i f).domain
r : R
eq1 : (↑x : N) = (↑a : N) + r • y
⊢ extensionToFun i f h x =
    HAdd.hAdd (β := Q) ((↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) a)
      ((extendIdealTo i f h y : (a : R) → Q) r : Q)
have obtain : ∀ (a : N) (ha : a ∈ (extensionOfMax i f).domain)
  (eq1 : (↑x : N) = (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) a ha) : N) + r • y),
  extensionToFun i f h x =
    HAdd.hAdd (β := Q)
      ((↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) a ha))
      ((extendIdealTo i f h y : (a : R) → Q) r : Q)
Tactic: obtain ⟨a, ha⟩ := a
Cleared hypotheses: a, eq1
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (hypothesis)
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 : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : (↑x : N) = (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) a ha) : N) + r • y
⊢ (↑(fst i x) : N) - a = (r - snd i x) • y
have eq1₁ : (↑x : N) = a + r • y
Tactic: change x = a + r • y at eq1
Cleared hypotheses: eq1
-- 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 : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : (↑x : N) = a + r • y
⊢ (↑(fst i x) : N) - a = (r - snd i x) • y
have rwa : ∀ (eq1 : (↑(fst i x) : N) + snd i x • y = a + r • y), (↑(fst i x) : N) - a = (r - snd i x) • y
Tactic: rwa [ExtensionOfMaxAdjoin.eqn, ← sub_eq_zero, ← sub_sub_sub_eq, sub_eq_zero, ← sub_smul]
      at eq1
Cleared hypotheses: eq1
-- 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 : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : (↑x : N) = a + r • y
rwa : ∀ (eq1 : (↑(fst i x) : N) + snd i x • y = a + r • y), (↑(fst i x) : N) - a = (r - snd i x) • y
⊢ (↑(fst i x) : N) - a = (r - snd i x) • y
have rwa₁ : ∀ (eq1 : (↑(fst i x) : N) + snd i x • y - (a + r • y) = 0), (↑(fst i x) : N) - a = (r - snd i x) • y
Tactic: rwa [ExtensionOfMaxAdjoin.eqn, ← sub_eq_zero, ← sub_sub_sub_eq, sub_eq_zero, ← sub_smul]
      at eq1
Cleared hypotheses: eq1
-- 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 : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : (↑x : N) = a + r • y
rwa : ∀ (eq1 : (↑(fst i x) : N) + snd i x • y = a + r • y), (↑(fst i x) : N) - a = (r - snd i x) • y
rwa₁ : ∀ (eq1 : (↑(fst i x) : N) + snd i x • y - (a + r • y) = 0), (↑(fst i x) : N) - a = (r - snd i x) • y
⊢ (↑(fst i x) : N) - a = (r - snd i x) • y
have rwa₂ : ∀ (eq1 : (↑(fst i x) : N) - a - (r • y - snd i x • y) = 0), (↑(fst i x) : N) - a = (r - snd i x) • y
Tactic: rwa [ExtensionOfMaxAdjoin.eqn, ← sub_eq_zero, ← sub_sub_sub_eq, sub_eq_zero, ← sub_smul]
      at eq1
Cleared hypotheses: eq1