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
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

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
-- 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)
eq1 :
  (↑a : N) + (↑b : N) =
    (↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) : N) +
      (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y
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
⊢ ExtensionOfMaxAdjoin.extensionToFun i f h (a + b) =
    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]

Premises used: Module.Baer.ExtensionOfMaxAdjoin.extensionToFun_wd, map_add, LinearPMap.map_add, HAdd.hAdd
-- 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)
eq1 :
  (↑a : N) + (↑b : N) =
    (↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) : N) +
      (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y
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)
⊢ (↑(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:
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
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) =
    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:
abel
-- 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
a : ↥(supExtensionOfMaxSingleton i f y)
dsimp : ExtensionOfMaxAdjoin.extensionToFun i f h (r • a) = r • ExtensionOfMaxAdjoin.extensionToFun i f h a
⊢ ExtensionOfMaxAdjoin.extensionToFun i f h (r • a) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (ExtensionOfMaxAdjoin.extensionToFun i f h a)

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
r : R
a : ↥(supExtensionOfMaxSingleton i f y)
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
⊢ r • (↑a : N) = (↑(r • ExtensionOfMaxAdjoin.fst i a) : N) + (r • ExtensionOfMaxAdjoin.snd i a) • y

Tactic:
rw [ExtensionOfMaxAdjoin.eqn, smul_add, smul_eq_mul, mul_smul]

Premises used: smul_eq_mul, Module.Baer.ExtensionOfMaxAdjoin.eqn, SemigroupAction.mul_smul, smul_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
r : R
a : ↥(supExtensionOfMaxSingleton i f y)
⊢ 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:
rfl
-- 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
a : ↥(supExtensionOfMaxSingleton i f y)
⊢ 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
-- 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
a : ↥(supExtensionOfMaxSingleton i f y)
eq1 : r • (↑a : N) = (↑(r • ExtensionOfMaxAdjoin.fst i a) : N) + (r • ExtensionOfMaxAdjoin.snd i a) • y
rw :
  r •
      HAdd.hAdd (β := Q)
        ((↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) (ExtensionOfMaxAdjoin.fst i a))
        ((ExtensionOfMaxAdjoin.extendIdealTo i f h y : (a : R) → Q) (ExtensionOfMaxAdjoin.snd i a) : Q) =
    r • ExtensionOfMaxAdjoin.extensionToFun i f h a
⊢ ExtensionOfMaxAdjoin.extensionToFun i f h (r • a) = r • ExtensionOfMaxAdjoin.extensionToFun i f h a

Tactic:
rw [ExtensionOfMaxAdjoin.extensionToFun_wd i f h (r • a :) _ _ eq1, map_smul,
          LinearPMap.map_smul, ← smul_add]

Premises used: Module.Baer.ExtensionOfMaxAdjoin.extensionToFun_wd, LinearPMap.map_smul, HSMul.hSMul, smul_add, map_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
a : ↥(supExtensionOfMaxSingleton i f y)
eq1 : r • (↑a : N) = (↑(r • ExtensionOfMaxAdjoin.fst i a) : N) + (r • ExtensionOfMaxAdjoin.snd i a) • y
⊢ r •
      HAdd.hAdd (β := Q)
        ((↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) (ExtensionOfMaxAdjoin.fst i a))
        ((ExtensionOfMaxAdjoin.extendIdealTo i f h y : (a : R) → Q) (ExtensionOfMaxAdjoin.snd i a) : Q) =
    r • ExtensionOfMaxAdjoin.extensionToFun i f h a

Tactic:
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
m : M
dsimp :
  (f : (a : M) → Q) m =
    ExtensionOfMaxAdjoin.extensionToFun i f h (y := y)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ supExtensionOfMaxSingleton i f y) ((i : (a : M) → N) m) ⋯)
⊢ (f : (a : M) → Q) m =
    (↑{ domain := supExtensionOfMaxSingleton i f y,
            toFun :=
              { toFun := ExtensionOfMaxAdjoin.extensionToFun i f h, map_add' := ⋯, map_smul' := ⋯ :
                LinearMap.{u, u, u_2, v} (RingHom.id R) (↥(supExtensionOfMaxSingleton i f y)) Q } :
            N →ₗ.[R] Q } :
        ↥{ domain := supExtensionOfMaxSingleton i f y,
                toFun :=
                  { toFun := ExtensionOfMaxAdjoin.extensionToFun i f h, map_add' := ⋯, map_smul' := ⋯ } }.domain →
          Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ supExtensionOfMaxSingleton i f y) ((i : (a : M) → N) m) ⋯)

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
m : M
rw :
  (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ supExtensionOfMaxSingleton i f y) ((i : (a : M) → N) m) ⋯) : N) =
    HAdd.hAdd (α := N)
      ((↑(Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((i : (a : M) → N) m) ⋯) : N) : N)
      (HSMul.hSMul.{u, u_2, u_2} (α := R) 0 y)
⊢ (f : (a : M) → Q) m =
    ExtensionOfMaxAdjoin.extensionToFun i f h (y := y)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ supExtensionOfMaxSingleton i f y) ((i : (a : M) → N) m) ⋯)

Tactic:
rw [(extensionOfMax i f).is_extension,
      ExtensionOfMaxAdjoin.extensionToFun_wd i f h _ ⟨i m, _⟩ 0 _, map_zero, add_zero]

Premises used: Module.Baer.ExtensionOfMaxAdjoin.extensionToFun_wd, Module.Baer.ExtensionOf.is_extension, map_zero, Subtype.mk, Module.Baer.extensionOfMax, add_zero, OfNat.ofNat, DFunLike.coe
-- 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
m : M
⊢ (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ supExtensionOfMaxSingleton i f y) ((i : (a : M) → N) m) ⋯) : N) =
    HAdd.hAdd (α := N)
      ((↑(Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax i f).domain) ((i : (a : M) → N) m) ⋯) : N) : N)
      (HSMul.hSMul.{u, u_2, u_2} (α := R) 0 y)

Tactic:
simp
-- 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 : ↥(extensionOfMax i f).domain
x' : ↥(extensionOfMaxAdjoin i f h y).domain
EQ : (↑x : N) = (↑x' : N)
symm :
  (↑(extensionOfMaxAdjoin i f h y).toLinearPMap : ↥(extensionOfMaxAdjoin i f h y).domain → Q) x' =
    (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x
⊢ (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x =
    (↑(extensionOfMaxAdjoin i f h y).toLinearPMap : ↥(extensionOfMaxAdjoin i f h y).domain → Q) x'

Tactic:
symm
-- 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 : ↥(extensionOfMax i f).domain
x' : ↥(extensionOfMaxAdjoin i f h y).domain
EQ : (↑x : N) = (↑x' : N)
change :
  ExtensionOfMaxAdjoin.extensionToFun i f h x' =
    (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x
⊢ (↑(extensionOfMaxAdjoin i f h y).toLinearPMap : ↥(extensionOfMaxAdjoin i f h y).domain → Q) x' =
    (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x

Tactic:
change ExtensionOfMaxAdjoin.extensionToFun i f h _ = _

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 : ↥(extensionOfMax i f).domain
x' : ↥(extensionOfMaxAdjoin i f h y).domain
EQ : (↑x : N) = (↑x' : N)
⊢ (↑x' : N) = (↑x : N) + HSMul.hSMul.{u, u_2, u_2} (α := R) 0 y

Tactic:
simp [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 : ↥(extensionOfMax i f).domain
x' : ↥(extensionOfMaxAdjoin i f h y).domain
EQ : (↑x : N) = (↑x' : N)
rw :
  HAdd.hAdd (β := Q) ((↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x)
      ((ExtensionOfMaxAdjoin.extendIdealTo i f h y : (a : R) → Q) 0 : Q) =
    (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x
rw₁ :
  (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x + 0 =
    (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x
rw₂ rw₃ :
  (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x =
    (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x
⊢ ExtensionOfMaxAdjoin.extensionToFun i f h x' =
    (↑(extensionOfMax i f).toLinearPMap : ↥(extensionOfMax i f).domain → Q) x

Tactic:
rw [ExtensionOfMaxAdjoin.extensionToFun_wd i f h x' x 0 (by simp [EQ]), map_zero,
      add_zero]

Premises used: Module.Baer.ExtensionOfMaxAdjoin.extensionToFun_wd, map_zero, add_zero, OfNat.ofNat
-- 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
⊢ (extensionOfMax i f).domain = ⊤

Tactic:
Submodule.eq_top_iff'.mpr fun y => ?_

Premises used: Iff.mpr, Submodule.eq_top_iff'
-- 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
refine : ∀ (y : N), y ∈ (extensionOfMax i f).domain
⊢ (extensionOfMax i f).domain = ⊤

Tactic:
refine Submodule.eq_top_iff'.mpr fun y => ?_

Premises used: Iff.mpr, Submodule.eq_top_iff'
-- 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
rw : ∃ y_1 ∈ (extensionOfMax i f).domain, ∃ (z : N), Membership.mem (γ := Submodule R N) (R ∙ y) z ∧ y_1 + z = y
y₁ : N
⊢ y ∈ (extensionOfMax i f).domain

Tactic:
rw [← extensionOfMax_is_max i f _ (extensionOfMax_le i f h), extensionOfMaxAdjoin,
    Submodule.mem_sup]

Premises used: Module.Baer.extensionOfMax_le, Module.Baer.extensionOfMaxAdjoin, Module.Baer.extensionOfMax_is_max, Submodule.mem_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))
h : Baer R Q
y : N
⊢ ∃ y_1 ∈ (extensionOfMax i f).domain, ∃ (z : N), Membership.mem (γ := Submodule R N) (R ∙ y) z ∧ y_1 + z = y

Tactic:
⟨0, Submodule.zero_mem _, y, Submodule.mem_span_singleton_self _, zero_add _⟩

Premises used: Submodule.mem_span_singleton_self, zero_add, Submodule.zero_mem, And.intro, Exists.intro, OfNat.ofNat
-- 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
h : Baer R Q
f : M →ₗ[R] N
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
g : M →ₗ[R] Q
this : Fact (Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N))
x y : N
rw :
  (↑(extensionOfMax f g).toLinearPMap : ↥(extensionOfMax f g).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax f g).domain) (x + y) ⋯) =
    (↑(extensionOfMax f g).toLinearPMap : ↥(extensionOfMax f g).domain → Q)
      (HAdd.hAdd (α := ↥(extensionOfMax f g).domain)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax f g).domain) x ⋯)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax f g).domain) y ⋯))
⊢ (↑(extensionOfMax f g).toLinearPMap : ↥(extensionOfMax f g).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax f g).domain) (x + y) ⋯) =
    (↑(extensionOfMax f g).toLinearPMap : ↥(extensionOfMax f g).domain → Q)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax f g).domain) x ⋯) +
      (↑(extensionOfMax f g).toLinearPMap : ↥(extensionOfMax f g).domain → Q)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax f g).domain) y ⋯)

Tactic:
rw [← LinearPMap.map_add]

Premises used: LinearPMap.map_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
h : Baer R Q
f : M →ₗ[R] N
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
g : M →ₗ[R] Q
this : Fact (Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N))
x y : N
⊢ (↑(extensionOfMax f g).toLinearPMap : ↥(extensionOfMax f g).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax f g).domain) (x + y) ⋯) =
    (↑(extensionOfMax f g).toLinearPMap : ↥(extensionOfMax f g).domain → Q)
      (HAdd.hAdd (α := ↥(extensionOfMax f g).domain)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax f g).domain) x ⋯)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax f g).domain) 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
h : Baer R Q
f : M →ₗ[R] N
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
g : M →ₗ[R] Q
this : Fact (Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N))
r : R
x : N
rw :
  (↑(extensionOfMax f g).toLinearPMap : ↥(extensionOfMax f g).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax f g).domain) (r • x) ⋯) =
    (↑(extensionOfMax f g).toLinearPMap : ↥(extensionOfMax f g).domain → Q)
      (HSMul.hSMul (α := R) (β := ↥(extensionOfMax f g).domain) ((RingHom.id R : (a : R) → R) r : R)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax f g).domain) x ⋯))
⊢ (↑(extensionOfMax f g).toLinearPMap : ↥(extensionOfMax f g).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax f g).domain) (r • x) ⋯) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
      ((↑(extensionOfMax f g).toLinearPMap : ↥(extensionOfMax f g).domain → Q)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ (extensionOfMax f g).domain) x ⋯))

Tactic:
rw [← LinearPMap.map_smul]

Premises used: LinearPMap.map_smul