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
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
rwa₂ : ∀ (eq1 : (↑(fst i x) : N) - a - (r • y - snd i x • 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), (↑(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
rwa₂ : ∀ (eq1 : (↑(fst i x) : N) - a - (r • y - snd i x • y) = 0), (↑(fst i x) : N) - a = (r - snd i x) • y
rwa₃ : ∀ (eq1 : (↑(fst i x) : N) - a = r • y - snd i x • 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) - a = (r - snd i x) • 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 (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
⊢ 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)
have eq2 : (↑(fst i x) : N) - a = (r - snd i x) • y
Tactic: have eq2 :
    (ExtensionOfMaxAdjoin.fst i x - a : N) = (r - ExtensionOfMaxAdjoin.snd i x) • y := by
    change x = a + r • y at eq1
    rwa [ExtensionOfMaxAdjoin.eqn, ← sub_eq_zero, ← sub_sub_sub_eq, sub_eq_zero, ← sub_smul]
      at 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) = (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) a ha) : N) + r • y
eq2 : (↑(fst i x) : N) - a = (r - snd i x) • y
⊢ (r - snd i x) • y ∈ (extensionOfMax i f).domain
have rw : (↑(fst i x) : N) - a ∈ (extensionOfMax i f).domain
Tactic: rw [← eq2]
-- 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
eq2 : (↑(fst i x) : N) - a = (r - snd i x) • 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)
have eq3 : (extendIdealTo i f h y : (a : R) → Q) (r - snd i x) =
  (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
    (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((r - snd i x) • y) sorry)
Tactic: have eq3 :=
    ExtensionOfMaxAdjoin.extendIdealTo_eq i f h (r - ExtensionOfMaxAdjoin.snd i x)
      (by rw [← eq2]; exact Submodule.sub_mem _ (ExtensionOfMaxAdjoin.fst i x).2 ha)
-- 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
eq2 : (↑(fst i x) : N) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y : (a : R) → Q) (r - snd i x) =
    (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((r - snd i x) • 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)
have eq3₁ : (extendIdealTo i f h y : (a : R) → Q) r =
  HAdd.hAdd (β := Q)
    ((↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) (r • y - snd i x • y) sorry))
    ((extendIdealTo i f h y : (a : R) → Q) (snd i x) : Q)
Tactic: simp only [map_sub, sub_smul, sub_eq_iff_eq_add] at eq3
Cleared hypotheses: eq3
-- 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) = (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) a ha) : N) + r • y
eq2 : (↑(fst i x) : N) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y : (a : R) → Q) r =
    HAdd.hAdd (β := Q)
      ((↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) (r • y - snd i x • y) ⋯))
      ((extendIdealTo i f h y : (a : R) → Q) (snd i x) : Q)
⊢ 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)
have unfold : HAdd.hAdd (β := Q) ((↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) (fst i x))
    ((extendIdealTo i f h y : (a : R) → Q) (snd i x) : Q) =
  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: unfold ExtensionOfMaxAdjoin.extensionToFun
-- 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) = (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) a ha) : N) + r • y
eq2 : (↑(fst i x) : N) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y : (a : R) → Q) r =
    HAdd.hAdd (β := Q)
      ((↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) (r • y - snd i x • y) ⋯))
      ((extendIdealTo i f h y : (a : R) → Q) (snd i x) : Q)
⊢ HAdd.hAdd (β := Q) ((↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) (fst i x))
      ((extendIdealTo i f h y : (a : R) → Q) (snd i x) : Q) =
    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)
have rw : HAdd.hAdd (β := Q) ((↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) (fst i x))
    ((extendIdealTo i f h y : (a : R) → Q) (snd i x) : Q) =
  HAdd.hAdd (β := Q)
    ((↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) (a + (r • y - snd i x • y)) sorry))
    ((extendIdealTo i f h y : (a : R) → Q) (snd i x) : Q)
Tactic: rw [eq3, ← add_assoc, ← (extensionOfMax i f).toLinearPMap.map_add, AddMemClass.mk_add_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))
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
eq2 : (↑(fst i x) : N) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y : (a : R) → Q) r =
    HAdd.hAdd (β := Q)
      ((↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) (r • y - snd i x • y) ⋯))
      ((extendIdealTo i f h y : (a : R) → Q) (snd i x) : Q)
⊢ HAdd.hAdd (β := Q) ((↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) (fst i x))
      ((extendIdealTo i f h y : (a : R) → Q) (snd i x) : Q) =
    HAdd.hAdd (β := Q)
      ((↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) (a + (r • y - snd i x • y)) ⋯))
      ((extendIdealTo i f h y : (a : R) → Q) (snd i x) : Q)
have e_a : fst i x = Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) (a + (r • y - snd i x • y)) sorry
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))
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
eq2 : (↑(fst i x) : N) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y : (a : R) → Q) r =
    HAdd.hAdd (β := Q)
      ((↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) (r • y - snd i x • y) ⋯))
      ((extendIdealTo i f h y : (a : R) → Q) (snd i x) : Q)
⊢ fst i x = Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) (a + (r • y - snd i x • y)) ⋯
have e_a : (↑(fst i x) : N) =
  (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) (a + (r • y - snd i x • y)) sorry) : N)
Tactic: ext
-- 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) = (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) a ha) : N) + r • y
eq2 : (↑(fst i x) : N) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y : (a : R) → Q) r =
    HAdd.hAdd (β := Q)
      ((↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) (r • y - snd i x • y) ⋯))
      ((extendIdealTo i f h y : (a : R) → Q) (snd i x) : Q)
⊢ (↑(fst i x) : N) =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) (a + (r • y - snd i x • y)) ⋯) : N)
have e_a : (↑(fst i x) : N) = a + (r • y - snd i x • y)
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
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
eq2 : (↑(fst i x) : N) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y : (a : R) → Q) r =
    HAdd.hAdd (β := Q)
      ((↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) (r • y - snd i x • y) ⋯))
      ((extendIdealTo i f h y : (a : R) → Q) (snd i x) : Q)
⊢ (↑(fst i x) : N) = a + (r • y - snd i x • y)
have e_a : (↑(fst i x) : N) = (↑x : N) - snd i x • y
Tactic: rw [Subtype.coe_mk, add_sub, ← 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
a b : ↥(supExtensionOfMaxSingleton i f y)
⊢ (↑a : N) + (↑b : N) =
    (↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) : N) +
      (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y
have rw : (↑(ExtensionOfMaxAdjoin.fst i a) : N) + ExtensionOfMaxAdjoin.snd i a • y +
    ((↑(ExtensionOfMaxAdjoin.fst i b) : N) + ExtensionOfMaxAdjoin.snd i b • y) =
  (↑(ExtensionOfMaxAdjoin.fst i a) : N) + (↑(ExtensionOfMaxAdjoin.fst i b) : N) +
    (ExtensionOfMaxAdjoin.snd i a • y + ExtensionOfMaxAdjoin.snd i b • y)
Tactic: rw [ExtensionOfMaxAdjoin.eqn, ExtensionOfMaxAdjoin.eqn, add_smul, Submodule.coe_add]
-- 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
a b : ↥(supExtensionOfMaxSingleton i f y)
⊢ ExtensionOfMaxAdjoin.extensionToFun i f h (a + b) =
    ExtensionOfMaxAdjoin.extensionToFun i f h a + ExtensionOfMaxAdjoin.extensionToFun i f h b
have eq1 : (↑a : N) + (↑b : N) =
  (↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) : N) +
    (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y
Tactic: have eq1 :
          ↑a + ↑b =
            ↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) +
              (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y := by
          rw [ExtensionOfMaxAdjoin.eqn, ExtensionOfMaxAdjoin.eqn, add_smul, Submodule.coe_add]
          ac_rfl
-- 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
a b : ↥(supExtensionOfMaxSingleton i f y)
eq1 :
  (↑a : N) + (↑b : N) =
    (↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) : N) +
      (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y
⊢ ExtensionOfMaxAdjoin.extensionToFun i f h (a + b) =
    ExtensionOfMaxAdjoin.extensionToFun i f h a + ExtensionOfMaxAdjoin.extensionToFun i f h b
have rw : (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) (ExtensionOfMaxAdjoin.fst i a) +
      (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) (ExtensionOfMaxAdjoin.fst i b) +
    HAdd.hAdd (α := Q) (β := Q)
      ((ExtensionOfMaxAdjoin.extendIdealTo i f h y : (a : R) → Q) (ExtensionOfMaxAdjoin.snd i a) : Q)
      ((ExtensionOfMaxAdjoin.extendIdealTo i f h y : (a : R) → Q) (ExtensionOfMaxAdjoin.snd i b) : Q) =
  ExtensionOfMaxAdjoin.extensionToFun i f h a + ExtensionOfMaxAdjoin.extensionToFun i f h b
Tactic: rw [ExtensionOfMaxAdjoin.extensionToFun_wd (y := y) i f h (a + b) _ _ eq1,
          LinearPMap.map_add, 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))
h : Baer R Q
y : N
a b : ↥(supExtensionOfMaxSingleton i f y)
eq1 :
  (↑a : N) + (↑b : N) =
    (↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) : N) +
      (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y
⊢ (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) (ExtensionOfMaxAdjoin.fst i a) +
        (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) (ExtensionOfMaxAdjoin.fst i b) +
      HAdd.hAdd (α := Q) (β := Q)
        ((ExtensionOfMaxAdjoin.extendIdealTo i f h y : (a : R) → Q) (ExtensionOfMaxAdjoin.snd i a) : Q)
        ((ExtensionOfMaxAdjoin.extendIdealTo i f h y : (a : R) → Q) (ExtensionOfMaxAdjoin.snd i b) : Q) =
    ExtensionOfMaxAdjoin.extensionToFun i f h a + ExtensionOfMaxAdjoin.extensionToFun i f h b
have unfold : (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) (ExtensionOfMaxAdjoin.fst i a) +
      (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) (ExtensionOfMaxAdjoin.fst i b) +
    HAdd.hAdd (α := Q) (β := Q)
      ((ExtensionOfMaxAdjoin.extendIdealTo i f h y : (a : R) → Q) (ExtensionOfMaxAdjoin.snd i a) : Q)
      ((ExtensionOfMaxAdjoin.extendIdealTo i f h y : (a : R) → Q) (ExtensionOfMaxAdjoin.snd i b) : Q) =
  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) +
    HAdd.hAdd (β := Q)
      ((↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) (ExtensionOfMaxAdjoin.fst i b))
      ((ExtensionOfMaxAdjoin.extendIdealTo i f h y : (a : R) → Q) (ExtensionOfMaxAdjoin.snd i b) : Q)
Tactic: unfold ExtensionOfMaxAdjoin.extensionToFun
-- 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)
⊢ ExtensionOfMaxAdjoin.extensionToFun i f h (r • a) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (ExtensionOfMaxAdjoin.extensionToFun i f h a)
have dsimp : ExtensionOfMaxAdjoin.extensionToFun i f h (r • a) = r • ExtensionOfMaxAdjoin.extensionToFun i f h a
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
r : R
a : ↥(supExtensionOfMaxSingleton i f y)
⊢ r • (↑a : N) = (↑(r • ExtensionOfMaxAdjoin.fst i a) : N) + (r • ExtensionOfMaxAdjoin.snd i a) • y
have rw : r • (↑(ExtensionOfMaxAdjoin.fst i a) : N) + r • ExtensionOfMaxAdjoin.snd i a • y =
  (↑(r • ExtensionOfMaxAdjoin.fst i a) : N) + r • ExtensionOfMaxAdjoin.snd i a • y
Tactic: rw [ExtensionOfMaxAdjoin.eqn, smul_add, smul_eq_mul, mul_smul]
-- 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
a : ↥(supExtensionOfMaxSingleton i f y)
⊢ ExtensionOfMaxAdjoin.extensionToFun i f h (r • a) = r • ExtensionOfMaxAdjoin.extensionToFun i f h a
have eq1 : r • (↑a : N) = (↑(r • ExtensionOfMaxAdjoin.fst i a) : N) + (r • ExtensionOfMaxAdjoin.snd i a) • y
Tactic: have eq1 :
          r • (a : N) =
            ↑(r • ExtensionOfMaxAdjoin.fst i a) + (r • ExtensionOfMaxAdjoin.snd i a) • y := by
          rw [ExtensionOfMaxAdjoin.eqn, smul_add, smul_eq_mul, mul_smul]
          rfl