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
X1 X2 : ExtensionOf i f
x : M
rw :
  (f : (a : M) → Q) x =
    (↑X2.toLinearPMap : ↥X2.domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ X2.domain) ((i : (a : M) → N) x) ⋯)
rw₁ rw₂ : Eq.{v + 1} (α := Q) ((f : (a : M) → Q) x : Q) ((f : (a : M) → Q) x : Q)
⊢ (↑X1.toLinearPMap : ↥X1.domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ X1.domain) ((i : (a : M) → N) x) ⋯) =
    (↑X2.toLinearPMap : ↥X2.domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ X2.domain) ((i : (a : M) → N) x) ⋯)

Tactic:
rw [← X1.is_extension x, ← X2.is_extension x]

Premises used: Module.Baer.ExtensionOf.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
X Y : ExtensionOf i f
x : N
y : x ∈ (X ⊓ Y).domain
h : x ∈ (X.toLinearPMap ⊓ Y.toLinearPMap).domain
⊢ (↑(X ⊓ Y).toLinearPMap : ↥(X ⊓ Y).domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ (X ⊓ Y).domain) x y) =
    (↑(X.toLinearPMap ⊓ Y.toLinearPMap) : ↥(X.toLinearPMap ⊓ Y.toLinearPMap).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ (X.toLinearPMap ⊓ Y.toLinearPMap).domain) x h)

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
c : Set (ExtensionOf i f)
hchain : IsChain (fun (x1 x2 : ExtensionOf i f) ↦ x1 ≤ x2) c
a : ExtensionOf i f
a_mem : a ∈ c
b : ExtensionOf i f
b_mem : b ∈ c
ne :
  Ne (α := N →ₗ.[R] Q) ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) a) ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) b)
⊢ (fun (x1 x2 : N →ₗ.[R] Q) ↦ x1 ≤ x2) ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) a)
      ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) b) ∨
    (fun (x1 x2 : N →ₗ.[R] Q) ↦ x1 ≤ x2) ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) b)
      ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) a)

Tactic:
hchain a_mem b_mem (ne_of_apply_ne _ ne)

Premises used: Set.Mem, ne_of_apply_ne
-- 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
c : Set (ExtensionOf i f)
hchain : IsChain (fun (x1 x2 : ExtensionOf i f) ↦ x1 ≤ x2) c
a : ExtensionOf i f
a_mem : a ∈ c
b : ExtensionOf i f
b_mem : b ∈ c
ne :
  Ne (α := N →ₗ.[R] Q) ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) a) ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) b)
⊢ (fun (x1 x2 : N →ₗ.[R] Q) ↦ x1 ≤ x2) ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) a)
      ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) b) ∨
    (fun (x1 x2 : N →ₗ.[R] Q) ↦ x1 ≤ x2) ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) b)
      ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) a)

Tactic:
exact hchain a_mem b_mem (ne_of_apply_ne _ ne)

Premises used: ne_of_apply_ne
-- 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
c : Set (ExtensionOf i f)
hchain : IsChain (fun (x1 x2 : ExtensionOf i f) ↦ x1 ≤ x2) c
hnonempty : c.Nonempty
⊢ i.range ≤ (LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) ⋯).domain

Tactic:
le_trans hnonempty.some.le <|
        (LinearPMap.le_sSup _ <|
            (Set.mem_image _ _ _).mpr ⟨hnonempty.some, hnonempty.choose_spec, rfl⟩).1

Premises used: Iff.mpr, Exists.choose_spec, Set.mem_image, And.left, And.intro, Exists.intro, Module.Baer.ExtensionOf.le, LinearPMap.le_sSup, rfl, Set.Nonempty.some, le_trans
-- 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
c : Set (ExtensionOf i f)
hchain : IsChain (fun (x1 x2 : ExtensionOf i f) ↦ x1 ≤ x2) c
hnonempty : c.Nonempty
⊢ i.range ≤ (LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) ⋯).domain

Tactic:
refine le_trans hnonempty.some.le <|
        (LinearPMap.le_sSup _ <|
            (Set.mem_image _ _ _).mpr ⟨hnonempty.some, hnonempty.choose_spec, rfl⟩).1

Premises used: Iff.mpr, Exists.choose_spec, Set.mem_image, And.left, And.intro, Exists.intro, Module.Baer.ExtensionOf.le, LinearPMap.le_sSup, rfl, Set.Nonempty.some, le_trans
-- 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
c : Set (ExtensionOf i f)
hchain : IsChain (fun (x1 x2 : ExtensionOf i f) ↦ x1 ≤ x2) c
hnonempty : c.Nonempty
m : M
⊢ (f : (a : M) → Q) m =
    (↑(LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) ⋯) :
        ↥(LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) ⋯).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦
        x ∈ (LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) ⋯).domain) ((i : (a : M) → N) m) ⋯)

Tactic:
Eq.trans (hnonempty.some.is_extension m) ?_

Premises used: Module.Baer.ExtensionOf.is_extension, Eq.trans, Set.Nonempty.some
-- 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
c : Set (ExtensionOf i f)
hchain : IsChain (fun (x1 x2 : ExtensionOf i f) ↦ x1 ≤ x2) c
hnonempty : c.Nonempty
m : M
refine :
  (↑hnonempty.some (s := c).toLinearPMap : ↥hnonempty.some.domain → Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ hnonempty.some (s := c).domain) ((i : (a : M) → N) m) ⋯) =
    (↑(LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) ⋯) :
        ↥(LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) ⋯).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦
        x ∈ (LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) ⋯).domain) ((i : (a : M) → N) m) ⋯)
⊢ (f : (a : M) → Q) m =
    (↑(LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) ⋯) :
        ↥(LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) ⋯).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦
        x ∈ (LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) ⋯).domain) ((i : (a : M) → N) m) ⋯)

Tactic:
refine Eq.trans (hnonempty.some.is_extension m) ?_

Premises used: Module.Baer.ExtensionOf.is_extension, Eq.trans, Set.Nonempty.some
-- 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
c : Set (ExtensionOf i f)
hchain : IsChain (fun (x1 x2 : ExtensionOf i f) ↦ x1 ≤ x2) c
hnonempty : c.Nonempty
m : M
symm :
  (↑(LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) ⋯) :
        ↥(LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) ⋯).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦
        x ∈ (LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) ⋯).domain) ((i : (a : M) → N) m) ⋯) =
    (↑hnonempty.some (s := c).toLinearPMap : ↥hnonempty.some.domain → Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ hnonempty.some (s := c).domain) ((i : (a : M) → N) m) ⋯)
⊢ (↑hnonempty.some (s := c).toLinearPMap : ↥hnonempty.some.domain → Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ hnonempty.some (s := c).domain) ((i : (a : M) → N) m) ⋯) =
    (↑(LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) ⋯) :
        ↥(LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) ⋯).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦
        x ∈ (LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) ⋯).domain) ((i : (a : M) → N) m) ⋯)

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
c : Set (ExtensionOf i f)
hchain : IsChain (fun (x1 x2 : ExtensionOf i f) ↦ x1 ≤ x2) c
hnonempty : c.Nonempty
m : M
⊢ DirectedOn (fun (x1 x2 : N →ₗ.[R] Q) ↦ x1 ≤ x2) ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c)

Tactic:
generalize_proofs _ _ h1
-- 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
c : Set (ExtensionOf i f)
hchain : IsChain (fun (x1 x2 : ExtensionOf i f) ↦ x1 ≤ x2) c
hnonempty : c.Nonempty
m : M
pf : DirectedOn (fun (x1 x2 : N →ₗ.[R] Q) ↦ x1 ≤ x2) ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c)
⊢ Membership.mem (α := N) (LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) pf).domain
    ((i : (a : M) → N) m : N)

Tactic:
generalize_proofs _ _ h1
-- 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
c : Set (ExtensionOf i f)
hchain : IsChain (fun (x1 x2 : ExtensionOf i f) ↦ x1 ≤ x2) c
hnonempty : c.Nonempty
m : M
pf : DirectedOn (fun (x1 x2 : N →ₗ.[R] Q) ↦ x1 ≤ x2) ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c)
pf₁ :
  Membership.mem (α := N) (LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) pf).domain
    ((i : (a : M) → N) m : N)
⊢ Membership.mem (α := N) hnonempty.some (s := c).domain ((i : (a : M) → N) m : N)

Tactic:
generalize_proofs _ _ h1
-- 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
c : Set (ExtensionOf i f)
hchain : IsChain (fun (x1 x2 : ExtensionOf i f) ↦ x1 ≤ x2) c
hnonempty : c.Nonempty
m : M
pf : DirectedOn (fun (x1 x2 : N →ₗ.[R] Q) ↦ x1 ≤ x2) ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c)
pf_1 :
  Membership.mem (α := N) (LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) pf).domain
    ((i : (a : M) → N) m : N)
h1 : Membership.mem (α := N) hnonempty.some (s := c).domain ((i : (a : M) → N) m : N)
⊢ (↑(LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) pf) :
        ↥(LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) pf).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦
        x ∈ (LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) pf).domain) ((i : (a : M) → N) m)
        pf_1) =
    (↑hnonempty.some (s := c).toLinearPMap : ↥hnonempty.some.domain → Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ hnonempty.some (s := c).domain) ((i : (a : M) → N) m) h1)

Tactic:
LinearPMap.sSup_apply (IsChain.directedOn <| chain_linearPMap_of_chain_extensionOf hchain)
          ((Set.mem_image _ _ _).mpr ⟨hnonempty.some, hnonempty.choose_spec, rfl⟩) ⟨i m, h1⟩

Premises used: Iff.mpr, Module.Baer.chain_linearPMap_of_chain_extensionOf, Exists.choose_spec, Set.Mem, Set.mem_image, LinearPMap.sSup_apply, IsChain.directedOn, Subtype.mk, And.intro, Exists.intro, DFunLike.coe, rfl, Set.Nonempty.some
-- 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
c : Set (ExtensionOf i f)
hchain : IsChain (fun (x1 x2 : ExtensionOf i f) ↦ x1 ≤ x2) c
hnonempty : c.Nonempty
m : M
pf : DirectedOn (fun (x1 x2 : N →ₗ.[R] Q) ↦ x1 ≤ x2) ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c)
pf_1 :
  Membership.mem (α := N) (LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) pf).domain
    ((i : (a : M) → N) m : N)
h1 : Membership.mem (α := N) hnonempty.some (s := c).domain ((i : (a : M) → N) m : N)
⊢ (↑(LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) pf) :
        ↥(LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) pf).domain → Q)
      (Subtype.mk (p := fun (x : N) ↦
        x ∈ (LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) pf).domain) ((i : (a : M) → N) m)
        pf_1) =
    (↑hnonempty.some (s := c).toLinearPMap : ↥hnonempty.some.domain → Q)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ hnonempty.some (s := c).domain) ((i : (a : M) → N) m) h1)

Tactic:
exact
        LinearPMap.sSup_apply (IsChain.directedOn <| chain_linearPMap_of_chain_extensionOf hchain)
          ((Set.mem_image _ _ _).mpr ⟨hnonempty.some, hnonempty.choose_spec, rfl⟩) ⟨i m, h1⟩

Premises used: Iff.mpr, Module.Baer.chain_linearPMap_of_chain_extensionOf, Exists.choose_spec, Set.mem_image, LinearPMap.sSup_apply, IsChain.directedOn, Subtype.mk, And.intro, Exists.intro, DFunLike.coe, rfl, Set.Nonempty.some
-- 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
c : Set (ExtensionOf i f)
hchain : IsChain (fun (x1 x2 : ExtensionOf i f) ↦ x1 ≤ x2) c
hnonempty : c.Nonempty
a : ExtensionOf i f
ha : a ∈ c
⊢ a ≤ max (c := c) hchain hnonempty

Tactic:
LinearPMap.le_sSup (IsChain.directedOn <| chain_linearPMap_of_chain_extensionOf hchain) <|
    (Set.mem_image _ _ _).mpr ⟨a, ha, rfl⟩

Premises used: Iff.mpr, Module.Baer.chain_linearPMap_of_chain_extensionOf, Set.Mem, Set.mem_image, IsChain.directedOn, LinearPMap.sSup, And.intro, Exists.intro, LinearPMap.le_sSup, 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))
x y : ↥i.range
⊢ HAdd.hAdd (α := N) (β := N)
      ((i : (a : M) → N) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) ⋯) : N)
      ((i : (a : M) → N) (Exists.choose (p := fun (y_1 : M) ↦ (i : (a : M) → N) y_1 = (↑y : N)) ⋯) : N) =
    (↑(x + y) : N)

Tactic:
have eq1 : _ + _ = (x + y).1 := congr_arg₂ (· + ·) x.2.choose_spec y.2.choose_spec
-- 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))
x y : ↥i.range
eq1 :
  HAdd.hAdd (α := N) (β := N)
      ((i : (a : M) → N) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) ⋯) : N)
      ((i : (a : M) → N) (Exists.choose (p := fun (y_1 : M) ↦ (i : (a : M) → N) y_1 = (↑y : N)) ⋯) : N) =
    (↑(x + y) : N)
⊢ Eq.{u_2 + 1} (α := N)
    ((i : (a : M) → N)
        (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) ⋯ +
          Exists.choose (p := fun (y_1 : M) ↦ (i : (a : M) → N) y_1 = (↑y : N)) ⋯) :
      N)
    ((i : (a : M) → N) (Exists.choose (p := fun (y_1 : M) ↦ (i : (a : M) → N) y_1 = (↑(x + y) : N)) ⋯) : N)

Tactic:
rw [← map_add, ← (x + y).2.choose_spec] at eq1

Premises used: Exists.choose_spec, map_add, HAdd.hAdd, 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))
x y : ↥i.range
eq1 :
  Eq.{u_2 + 1} (α := N)
    ((i : (a : M) → N)
        (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) ⋯ +
          Exists.choose (p := fun (y_1 : M) ↦ (i : (a : M) → N) y_1 = (↑y : N)) ⋯) :
      N)
    ((i : (a : M) → N) (Exists.choose (p := fun (y_1 : M) ↦ (i : (a : M) → N) y_1 = (↑(x + y) : N)) ⋯) : N)
dsimp :
  (f : (a : M) → Q) (Exists.choose (p := fun (y_1 : M) ↦ (i : (a : M) → N) y_1 = (↑x : N) + (↑y : N)) ⋯) =
    HAdd.hAdd (α := Q) (β := Q)
      ((f : (a : M) → Q) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) ⋯) : Q)
      ((f : (a : M) → Q) (Exists.choose (p := fun (y_1 : M) ↦ (i : (a : M) → N) y_1 = (↑y : N)) ⋯) : Q)
⊢ (f : (a : M) → Q) (Exists.choose (p := fun (y_1 : M) ↦ (i : (a : M) → N) y_1 = (↑(x + y) : N)) ⋯) =
    HAdd.hAdd (α := Q) (β := Q)
      ((f : (a : M) → Q) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) ⋯) : Q)
      ((f : (a : M) → Q) (Exists.choose (p := fun (y_1 : M) ↦ (i : (a : M) → N) y_1 = (↑y : N)) ⋯) : 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))
x y : ↥i.range
eq1 :
  Eq.{u_2 + 1} (α := N)
    ((i : (a : M) → N)
        (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) ⋯ +
          Exists.choose (p := fun (y_1 : M) ↦ (i : (a : M) → N) y_1 = (↑y : N)) ⋯) :
      N)
    ((i : (a : M) → N) (Exists.choose (p := fun (y_1 : M) ↦ (i : (a : M) → N) y_1 = (↑(x + y) : N)) ⋯) : N)
rw :
  (f : (a : M) → Q)
      (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) ⋯ +
        Exists.choose (p := fun (y_1 : M) ↦ (i : (a : M) → N) y_1 = (↑y : N)) ⋯) =
    HAdd.hAdd (α := Q) (β := Q)
      ((f : (a : M) → Q) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) ⋯) : Q)
      ((f : (a : M) → Q) (Exists.choose (p := fun (y_1 : M) ↦ (i : (a : M) → N) y_1 = (↑y : N)) ⋯) : Q)
rw₁ rw₂ :
  HAdd.hAdd (α := Q) (β := Q)
      ((f : (a : M) → Q) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) ⋯) : Q)
      ((f : (a : M) → Q) (Exists.choose (p := fun (y_1 : M) ↦ (i : (a : M) → N) y_1 = (↑y : N)) ⋯) : Q) =
    HAdd.hAdd (α := Q) (β := Q)
      ((f : (a : M) → Q) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) ⋯) : Q)
      ((f : (a : M) → Q) (Exists.choose (p := fun (y_1 : M) ↦ (i : (a : M) → N) y_1 = (↑y : N)) ⋯) : Q)
⊢ (f : (a : M) → Q) (Exists.choose (p := fun (y_1 : M) ↦ (i : (a : M) → N) y_1 = (↑x : N) + (↑y : N)) ⋯) =
    HAdd.hAdd (α := Q) (β := Q)
      ((f : (a : M) → Q) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) ⋯) : Q)
      ((f : (a : M) → Q) (Exists.choose (p := fun (y_1 : M) ↦ (i : (a : M) → N) y_1 = (↑y : N)) ⋯) : Q)

Tactic:
rw [← Fact.out (p := Function.Injective i) eq1, map_add]

Premises used: map_add, Fact.out
-- 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))
r : R
x : ↥i.range
⊢ HSMul.hSMul (β := N) r ((i : (a : M) → N) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) ⋯) : N) =
    (↑(r • x) : N)

Tactic:
have eq1 : r • _ = (r • x).1 := congr_arg (r • ·) x.2.choose_spec
-- 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))
r : R
x : ↥i.range
eq1 :
  HSMul.hSMul (β := N) r ((i : (a : M) → N) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) ⋯) : N) =
    (↑(r • x) : N)
⊢ Eq.{u_2 + 1} (α := N)
    ((i : (a : M) → N) (r • Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) ⋯) : N)
    ((i : (a : M) → N) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑(r • x) : N)) ⋯) : N)

Tactic:
rw [← map_smul, ← (r • x).2.choose_spec] at eq1

Premises used: Exists.choose_spec, HSMul.hSMul, map_smul, 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))
r : R
x : ↥i.range
eq1 :
  Eq.{u_2 + 1} (α := N)
    ((i : (a : M) → N) (r • Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) ⋯) : N)
    ((i : (a : M) → N) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑(r • x) : N)) ⋯) : N)
dsimp :
  (f : (a : M) → Q) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = r • (↑x : N)) ⋯) =
    HSMul.hSMul (β := Q) r ((f : (a : M) → Q) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) ⋯) : Q)
⊢ (f : (a : M) → Q) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑(r • x) : N)) ⋯) =
    HSMul.hSMul (α := R) (β := Q) ((RingHom.id R : (a : R) → R) r : R)
      ((f : (a : M) → Q) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) ⋯) : 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))
r : R
x : ↥i.range
eq1 :
  Eq.{u_2 + 1} (α := N)
    ((i : (a : M) → N) (r • Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) ⋯) : N)
    ((i : (a : M) → N) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑(r • x) : N)) ⋯) : N)
rw :
  (f : (a : M) → Q) (r • Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) ⋯) =
    HSMul.hSMul (β := Q) r ((f : (a : M) → Q) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) ⋯) : Q)
rw₁ rw₂ :
  HSMul.hSMul (β := Q) r ((f : (a : M) → Q) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) ⋯) : Q) =
    HSMul.hSMul (β := Q) r ((f : (a : M) → Q) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) ⋯) : Q)
⊢ (f : (a : M) → Q) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = r • (↑x : N)) ⋯) =
    HSMul.hSMul (β := Q) r ((f : (a : M) → Q) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) ⋯) : Q)

Tactic:
rw [← Fact.out (p := Function.Injective i) eq1, map_smul]

Premises used: Fact.out, map_smul