awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Injective
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)

Tactic:
ExtensionOfMaxAdjoin.extendIdealTo_wd' i f h (r - r') _

Premises used: HSub.hSub, Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_wd'
-- Module: Mathlib.Algebra.Module.Injective
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 - r') • y = 0
⊢ Eq.{v + 1} (α := Q) ((extendIdealTo i f h y : (a : R) → Q) (r - r') : Q) (0 : Q)

Tactic:
convert! ExtensionOfMaxAdjoin.extendIdealTo_wd' i f h (r - r') _

Premises used: HSub.hSub, Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_wd'
-- Module: Mathlib.Algebra.Module.Injective
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
convert_2₂ convert_2₃ : r' • y = r' • y
⊢ (r - r') • y = 0

Tactic:
rw [sub_smul, sub_eq_zero, eq1]

Premises used: sub_eq_zero, sub_smul
-- Module: Mathlib.Algebra.Module.Injective
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
hr : r • y ∈ (extensionOfMax i f).domain
⊢ (extendIdealTo i f h y : (a : R) → Q) r =
    (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) (r • y) hr)

Tactic:
simp only [ExtensionOfMaxAdjoin.extendIdealTo_is_extension i f h _ _ hr,
    ExtensionOfMaxAdjoin.idealTo, LinearMap.coe_mk, AddHom.coe_mk]

Premises used: LinearMap.coe_mk, Module.Baer.ExtensionOfMaxAdjoin.idealTo, Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_is_extension, AddHom.coe_mk
-- Module: Mathlib.Algebra.Module.Injective
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
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)
⊢ 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)

Tactic:
obtain ⟨a, ha⟩ := a
-- Module: Mathlib.Algebra.Module.Injective
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
⊢ (↑x : N) = a + r • y

Tactic:
change x = a + r • y at eq1
-- Module: Mathlib.Algebra.Module.Injective
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
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (eq1 : (↑(fst i x) : N) - a = (r - snd i x) • y), (↑(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

Premises used: sub_eq_zero, sub_smul, Module.Baer.ExtensionOfMaxAdjoin.eqn, sub_sub_sub_eq
-- Module: Mathlib.Algebra.Module.Injective
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

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
-- Module: Mathlib.Algebra.Module.Injective
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
rw : (↑(fst i x) : N) - a ∈ (extensionOfMax i f).domain
⊢ (r - snd i x) • y ∈ (extensionOfMax i f).domain

Tactic:
rw [← eq2]
-- Module: Mathlib.Algebra.Module.Injective
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
⊢ (↑(fst i x) : N) - a ∈ (extensionOfMax i f).domain

Tactic:
Submodule.sub_mem _ (ExtensionOfMaxAdjoin.fst i x).2 ha

Premises used: Module.Baer.ExtensionOfMaxAdjoin.fst, Submodule.sub_mem, Subtype.property
-- Module: Mathlib.Algebra.Module.Injective
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
⊢ (↑(fst i x) : N) - a ∈ (extensionOfMax i f).domain

Tactic:
exact Submodule.sub_mem _ (ExtensionOfMaxAdjoin.fst i x).2 ha

Premises used: Module.Baer.ExtensionOfMaxAdjoin.fst, Submodule.sub_mem, Subtype.property
-- Module: Mathlib.Algebra.Module.Injective
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
⊢ (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) ⋯)

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)
-- Module: Mathlib.Algebra.Module.Injective
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) ⋯)
⊢ (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)

Tactic:
simp only [map_sub, sub_smul, sub_eq_iff_eq_add] at eq3

Premises used: map_sub, sub_smul, sub_eq_iff_eq_add
-- Module: Mathlib.Algebra.Module.Injective
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)
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)
⊢ 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:
unfold ExtensionOfMaxAdjoin.extensionToFun

Premises used: Module.Baer.ExtensionOfMaxAdjoin.extensionToFun
-- Module: Mathlib.Algebra.Module.Injective
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)
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)) ⋯))
      ((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)

Tactic:
rw [eq3, ← add_assoc, ← (extensionOfMax i f).toLinearPMap.map_add, AddMemClass.mk_add_mk]

Premises used: add_assoc, LinearPMap.map_add, Module.Baer.ExtensionOf.toLinearPMap, Module.Baer.extensionOfMax, AddMemClass.mk_add_mk
-- Module: Mathlib.Algebra.Module.Injective
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)
e_a : fst i x = Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) (a + (r • y - snd i x • y)) ⋯
⊢ 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)

Tactic:
congr
-- Module: Mathlib.Algebra.Module.Injective
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)
e_a :
  (↑(fst i x) : N) =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) (a + (r • y - snd i x • y)) ⋯) : N)
⊢ fst i x = Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) (a + (r • y - snd i x • y)) ⋯

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Injective
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)
e_a : (↑(fst i x) : N) = a + (r • y - snd i x • y)
⊢ (↑(fst i x) : N) =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) (a + (r • y - snd i x • y)) ⋯) : N)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Module.Injective
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)
e_a : (↑(fst i x) : N) = (↑x : N) - snd i x • y
⊢ (↑(fst i x) : N) = a + (r • y - snd i x • y)

Tactic:
rw [Subtype.coe_mk, add_sub, ← eq1]

Premises used: Subtype.coe_mk, add_sub
-- Module: Mathlib.Algebra.Module.Injective
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) = (↑x : N) - snd i x • y

Tactic:
eq_sub_of_add_eq (ExtensionOfMaxAdjoin.eqn i x).symm

Premises used: eq_sub_of_add_eq, Eq.symm, Module.Baer.ExtensionOfMaxAdjoin.eqn
-- Module: Mathlib.Algebra.Module.Injective
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) = (↑x : N) - snd i x • y

Tactic:
exact eq_sub_of_add_eq (ExtensionOfMaxAdjoin.eqn i x).symm

Premises used: eq_sub_of_add_eq, Eq.symm, Module.Baer.ExtensionOfMaxAdjoin.eqn
-- Module: Mathlib.Algebra.Module.Injective
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)
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)
⊢ (↑a : N) + (↑b : N) =
    (↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) : N) +
      (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y

Tactic:
rw [ExtensionOfMaxAdjoin.eqn, ExtensionOfMaxAdjoin.eqn, add_smul, Submodule.coe_add]

Premises used: Submodule.coe_add, add_smul, Module.Baer.ExtensionOfMaxAdjoin.eqn
-- Module: Mathlib.Algebra.Module.Injective
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.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:
ac_rfl