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))
m : M
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)) ⋯),
            map_add' := ⋯ } :
          (a : ↥i.range) → Q)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ i.range) ((i : (a : M) → N) m) ⋯ : ↥i.range) :
      Q)
⊢ 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)

Tactic:
simp only [LinearPMap.mk_apply, LinearMap.coe_mk]

Premises used: LinearMap.coe_mk, LinearPMap.mk_apply
-- 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))
m : M
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))
          ⋯) :
      Q)
⊢ 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)

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))
m : M
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)) ⋯
⊢ 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)

Tactic:
apply congrArg

Premises used: congrArg
-- 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))
m : M
⊢ m = Exists.choose (p := fun (y : M) ↦ Eq.{u_2 + 1} (α := N) ((i : (a : M) → N) y : N) ((i : (a : M) → N) m : N)) ⋯

Tactic:
Fact.out (p := Function.Injective i)
          (⟨i m, ⟨_, rfl⟩⟩ : LinearMap.range i).2.choose_spec.symm

Premises used: Exists.choose_spec, Subtype.mk, Exists.intro, Eq.symm, DFunLike.coe, rfl, Fact.out, 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))
m : M
⊢ m = Exists.choose (p := fun (y : M) ↦ Eq.{u_2 + 1} (α := N) ((i : (a : M) → N) y : N) ((i : (a : M) → N) m : N)) ⋯

Tactic:
exact Fact.out (p := Function.Injective i)
          (⟨i m, ⟨_, rfl⟩⟩ : LinearMap.range i).2.choose_spec.symm

Premises used: Exists.choose_spec, Subtype.mk, Exists.intro, Eq.symm, DFunLike.coe, rfl, Fact.out, 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))
⊢ ∀ (a : ExtensionOf i f), extensionOfMax i f ≤ a → a = extensionOfMax i f

Tactic:
fun _ ↦ (@zorn_le_nonempty (ExtensionOf i f) _ ⟨Inhabited.default⟩ fun _ hchain hnonempty =>
    ⟨ExtensionOf.max hchain hnonempty, ExtensionOf.le_max hchain hnonempty⟩).choose_spec.eq_of_ge

Premises used: Exists.choose_spec, Set.Mem, Module.Baer.extensionOfMax, Exists.intro, Module.Baer.ExtensionOf.max, IsMax.eq_of_ge, zorn_le_nonempty, Module.Baer.ExtensionOf.le_max
-- 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))
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
⊢ (↑x : N) ∈ (↑(supExtensionOfMaxSingleton i f y) : Set N)

Tactic:
have mem1 : x.1 ∈ (_ : Set _) := x.2
-- 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))
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
mem1 : (↑x : N) ∈ (↑(supExtensionOfMaxSingleton i f y) : Set N)
⊢ (↑x : N) ∈ (↑(extensionOfMax i f).domain : Set N) + (↑(R ∙ y) : Set N)

Tactic:
rw [Submodule.coe_sup] at mem1

Premises used: Submodule.coe_sup
-- 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))
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
mem1 : (↑x : N) ∈ (↑(extensionOfMax i f).domain : Set N) + (↑(R ∙ y) : Set N)
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
⊢ ∃ (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⟩

Premises used: Submodule.span
-- 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))
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 : R), a • y = b

Tactic:
rw [Submodule.mem_span_singleton] at b_mem

Premises used: Submodule.mem_span_singleton
-- 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))
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)
b_mem₁ : ∃ (a : R), a • y = b
⊢ (fun (x1 x2 : N) ↦ x1 + x2) a b = (↑x : N)

Tactic:
rw [Submodule.mem_span_singleton] at b_mem

Premises used: Submodule.mem_span_singleton
-- 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))
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)
rcases : ∀ (z : R) (eq2 : z • y = b), ∃ (a : ↥(extensionOfMax i f).domain) (b : R), (↑x : N) = (↑a : N) + b • y
⊢ ∃ (a : ↥(extensionOfMax i f).domain) (b : R), (↑x : N) = (↑a : N) + b • y

Tactic:
rcases b_mem with ⟨z, 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))
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
rw₁ 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
⊢ (↑x : N) = (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) a a_mem) : N) + z • y

Tactic:
rw [← eq1, ← 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))
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
⊢ ∃ (a : ↥(extensionOfMax i f).domain) (b : R), (↑x : N) = (↑a : N) + b • y

Tactic:
exact ⟨⟨a, a_mem⟩, z, by rw [← eq1, ← 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))
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
⊢ (↑x : N) = (↑(fst i x) : N) + snd i x • y

Tactic:
(extensionOfMax_adjoin.aux1 i x).choose_spec.choose_spec

Premises used: Exists.choose_spec, _private.0.Module.Baer.extensionOfMax_adjoin.aux1
-- 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))
y : N
z1 z2 : ↥(ideal i f y)
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) ⋯) =
    (↑(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) ⋯)
⊢ (↑(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) ⋯)

Tactic:
simp_rw [← (extensionOfMax i f).toLinearPMap.map_add]

Premises used: LinearPMap.map_add, Module.Baer.ExtensionOf.toLinearPMap, Module.Baer.extensionOfMax
-- 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))
y : N
z1 z2 : ↥(ideal i f y)
e_a :
  (↑(z1 + z2) : R) • y =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((↑z1 : R) • y) ⋯) : N) +
      (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((↑z2 : R) • y) ⋯) : N)
⊢ (↑(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) ⋯)

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))
y : N
z1 z2 : ↥(ideal i f y)
⊢ (↑(z1 + z2) : R) • y =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((↑z1 : R) • y) ⋯) : N) +
      (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((↑z2 : R) • y) ⋯) : N)

Tactic:
apply add_smul

Premises used: add_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))
y : N
z1 : R
z2 : ↥(ideal i f y)
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) ⋯) =
    (↑(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) ⋯))
⊢ (↑(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) ⋯))

Tactic:
simp_rw [← (extensionOfMax i f).toLinearPMap.map_smul]

Premises used: Module.Baer.ExtensionOf.toLinearPMap, LinearPMap.map_smul, Module.Baer.extensionOfMax
-- 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))
y : N
z1 : R
z2 : ↥(ideal i f y)
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) ⋯) : N)
⊢ (↑(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) ⋯))

Tactic:
congr 2
-- 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))
y : N
z1 : R
z2 : ↥(ideal i f y)
⊢ (↑(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) ⋯) : N)

Tactic:
apply mul_smul

Premises used: SemigroupAction.mul_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
⊢ ∀ (x : R) (mem : x ∈ ideal i f y),
    Eq.{v + 1} (α := Q) ((extendIdealTo i f h y : (a : R) → Q) x : Q)
      ((idealTo i f y : (a : ↥(ideal i f y)) → Q) (Subtype.mk (p := fun (x : R) ↦ x ∈ ideal i f y) x mem) : Q)

Tactic:
(h (ExtensionOfMaxAdjoin.ideal i f y) (ExtensionOfMaxAdjoin.idealTo i f y)).choose_spec

Premises used: Exists.choose_spec, Module.Baer.ExtensionOfMaxAdjoin.idealTo, Module.Baer.ExtensionOfMaxAdjoin.ideal
-- 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
eq1 : r • y = 0
change : r • y ∈ (extensionOfMax i f).domain
⊢ r ∈ ideal i f y

Tactic:
change (r • y) ∈ (extensionOfMax i f).toLinearPMap.domain

Premises used: Module.Baer.ExtensionOf.toLinearPMap, Module.Baer.extensionOfMax, HSMul.hSMul, LinearPMap.domain
-- 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
eq1 : r • y = 0
rw : 0 ∈ (extensionOfMax i f).domain
⊢ r • y ∈ (extensionOfMax i f).domain

Tactic:
rw [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
r : R
eq1 : r • y = 0
⊢ 0 ∈ (extensionOfMax i f).domain

Tactic:
apply Submodule.zero_mem _

Premises used: Submodule.zero_mem
-- 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
eq1 : r • y = 0
⊢ 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 _
-- 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
eq1 : r • y = 0
this : r ∈ ideal i f y
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)
⊢ Eq.{v + 1} (α := Q) ((extendIdealTo i f h y : (a : R) → Q) r : Q) (0 : Q)

Tactic:
rw [ExtensionOfMaxAdjoin.extendIdealTo_is_extension i f h y r this]

Premises used: Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_is_extension
-- 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
eq1 : r • y = 0
this : r ∈ ideal i f y
dsimp :
  (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) (r • y) ⋯) =
    0
⊢ 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:
dsimp [ExtensionOfMaxAdjoin.idealTo]

Premises used: Module.Baer.ExtensionOfMaxAdjoin.idealTo
-- 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
eq1 : r • y = 0
this : r ∈ ideal i f y
⊢ (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) (r • y) ⋯) =
    0

Tactic:
simp only [eq1, ← ZeroMemClass.zero_def, (extensionOfMax i f).toLinearPMap.map_zero]

Premises used: ZeroMemClass.zero_def, LinearPMap.map_zero, Module.Baer.ExtensionOf.toLinearPMap, Module.Baer.extensionOfMax
-- 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
rw : Eq.{v + 1} (α := Q) ((extendIdealTo i f h y : (a : R) → Q) (r - r') : Q) (0 : Q)
⊢ Eq.{v + 1} (α := Q) ((extendIdealTo i f h y : (a : R) → Q) r : Q) ((extendIdealTo i f h y : (a : R) → Q) r' : Q)

Tactic:
rw [← sub_eq_zero, ← map_sub]

Premises used: map_sub, sub_eq_zero