awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
b : ExtensionOf i f
a : N →ₗ.[R] Q
a_le : i.range ≤ a.domain
e1 :
  ∀ (m : M),
    (f : (a : M) → Q) m = (↑a : ↥a.domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ a.domain) ((i : (a : M) → N) m) ⋯)
domain_eq : { toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f }.domain = b.domain
to_fun_eq :
  ∀ ⦃x : N⦄ ⦃ha : x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f }.domain⦄
    ⦃hb : x ∈ b.domain⦄,
    (↑{ toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f }.toLinearPMap :
          ↥{ toLinearPMap := a, le := a_le, is_extension := e1 }.domain → Q)
        (Subtype.mk (p := fun (x : N) ↦
          x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f }.domain) x ha) =
      (↑b.toLinearPMap : ↥b.domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ b.domain) x hb)
⊢ { toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f } = b
have e_toLinearPMap : a = b.toLinearPMap
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
x x_1 : ExtensionOf i f
h : x.toLinearPMap = x_1.toLinearPMap
⊢ x = x_1
have domain_eq : ∀ (x_2 : N), x_2 ∈ x.domain ↔ x_2 ∈ x_1.domain
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
x x_1 : ExtensionOf i f
h : x.toLinearPMap = x_1.toLinearPMap
domain_eq : ∀ (x_2 : N), x_2 ∈ x.domain ↔ x_2 ∈ x_1.domain
⊢ x = x_1
have to_fun_eq : ∀ ⦃x_2 : N⦄ ⦃ha : x_2 ∈ x.domain⦄ ⦃hb : x_2 ∈ x_1.domain⦄,
  (↑x.toLinearPMap : ↥x.domain → Q) (Subtype.mk (p := fun (x_3 : N) ↦ x_3 ∈ x.domain) x_2 ha) =
    (↑x_1.toLinearPMap : ↥x_1.domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ x_1.domain) x_2 hb)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
X1 X2 : ExtensionOf i f
x : N
hx : x ∈ i.range
⊢ x ∈ X1.eqLocus X2.toLinearPMap
have rcases : ∀ (x : M), Membership.mem (α := N) (X1.eqLocus X2.toLinearPMap) ((i : (a : M) → N) x : N)
Tactic: rcases hx with ⟨x, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
X1 X2 : ExtensionOf i f
x : M
⊢ Membership.mem (α := N) (X1.eqLocus X2.toLinearPMap) ((i : (a : M) → N) x : N)
have refine : (↑X1.toLinearPMap : ↥X1.domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ X1.domain) ((i : (a : M) → N) x) sorry) =
  (↑X2.toLinearPMap : ↥X2.domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ X2.domain) ((i : (a : M) → N) x) sorry)
Tactic: refine ⟨X1.le (Set.mem_range_self _), X2.le (Set.mem_range_self _), ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
X1 X2 : ExtensionOf i f
x : M
⊢ (↑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) ⋯)
have 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) sorry)
Tactic: rw [← X1.is_extension x, ← X2.is_extension x]
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
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) ⋯)
⊢ (↑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) ⋯)
have rw₁ : Eq.{v + 1} (α := Q) ((f : (a : M) → Q) x : Q) ((f : (a : M) → Q) x : Q)
Tactic: rw [← X1.is_extension x, ← X2.is_extension x]
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
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) ⋯)
have 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) sorry) =
  (↑(LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) sorry) :
      ↥(LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) sorry).domain → Q)
    (Subtype.mk (p := fun (x : N) ↦ x ∈ (LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) sorry).domain)
      ((i : (a : M) → N) m) sorry)
Tactic: refine Eq.trans (hnonempty.some.is_extension m) ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
c : Set (ExtensionOf i f)
hchain : IsChain (fun (x1 x2 : ExtensionOf i f) ↦ x1 ≤ x2) c
hnonempty : c.Nonempty
m : 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) ⋯)
have symm : (↑(LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) sorry) :
      ↥(LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) sorry).domain → Q)
    (Subtype.mk (p := fun (x : N) ↦ x ∈ (LinearPMap.sSup ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c) sorry).domain)
      ((i : (a : M) → N) m) sorry) =
  (↑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) sorry)
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (hypothesis)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
c : Set (ExtensionOf i f)
hchain : IsChain (fun (x1 x2 : ExtensionOf i f) ↦ x1 ≤ x2) c
hnonempty : c.Nonempty
m : 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) ⋯) =
    (↑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) ⋯)
have pf : DirectedOn (fun (x1 x2 : N →ₗ.[R] Q) ↦ x1 ≤ x2) ((fun (x : ExtensionOf i f) ↦ x.toLinearPMap) '' c)
Tactic: generalize_proofs _ _ h1
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (hypothesis)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
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)
⊢ (↑(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) ⋯)
have pf₁ : 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
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (hypothesis)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
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)
⊢ (↑(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) ⋯)
have h1 : Membership.mem (α := N) hnonempty.some (s := c).domain ((i : (a : M) → N) m : N)
Tactic: generalize_proofs _ _ h1
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (hypothesis)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst_7 : Fact (Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑i : (a : M) → N))
x y : ↥i.range
⊢ (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)
have eq1 : HAdd.hAdd (α := N) (β := N)
    ((i : (a : M) → N) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) sorry) : N)
    ((i : (a : M) → N) (Exists.choose (p := fun (y_1 : M) ↦ (i : (a : M) → N) y_1 = (↑y : N)) sorry) : N) =
  (↑(x + y) : N)
Tactic: have eq1 : _ + _ = (x + y).1 := congr_arg₂ (· + ·) x.2.choose_spec y.2.choose_spec
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (hypothesis)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst_7 : Fact (Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑i : (a : M) → N))
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)
⊢ (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)
have eq1₁ : Eq.{u_2 + 1} (α := N)
  ((i : (a : M) → N)
      (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) sorry +
        Exists.choose (p := fun (y_1 : M) ↦ (i : (a : M) → N) y_1 = (↑y : N)) sorry) :
    N)
  ((i : (a : M) → N) (Exists.choose (p := fun (y_1 : M) ↦ (i : (a : M) → N) y_1 = (↑(x + y) : N)) sorry) : N)
Tactic: rw [← map_add, ← (x + y).2.choose_spec] at eq1
Cleared hypotheses: eq1
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst_7 : Fact (Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑i : (a : M) → N))
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)
⊢ (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)
have rw : (f : (a : M) → Q)
    (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) sorry +
      Exists.choose (p := fun (y_1 : M) ↦ (i : (a : M) → N) y_1 = (↑y : N)) sorry) =
  HAdd.hAdd (α := Q) (β := Q)
    ((f : (a : M) → Q) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) sorry) : Q)
    ((f : (a : M) → Q) (Exists.choose (p := fun (y_1 : M) ↦ (i : (a : M) → N) y_1 = (↑y : N)) sorry) : Q)
Tactic: rw [← Fact.out (p := Function.Injective i) eq1, map_add]
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst_7 : Fact (Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑i : (a : M) → N))
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)
⊢ (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)
have rw₁ : HAdd.hAdd (α := Q) (β := Q)
    ((f : (a : M) → Q) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) sorry) : Q)
    ((f : (a : M) → Q) (Exists.choose (p := fun (y_1 : M) ↦ (i : (a : M) → N) y_1 = (↑y : N)) sorry) : Q) =
  HAdd.hAdd (α := Q) (β := Q)
    ((f : (a : M) → Q) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) sorry) : Q)
    ((f : (a : M) → Q) (Exists.choose (p := fun (y_1 : M) ↦ (i : (a : M) → N) y_1 = (↑y : N)) sorry) : Q)
Tactic: rw [← Fact.out (p := Function.Injective i) eq1, map_add]
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (hypothesis)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst_7 : Fact (Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑i : (a : M) → N))
r : R
x : ↥i.range
⊢ (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)
have eq1 : HSMul.hSMul (β := N) r ((i : (a : M) → N) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) sorry) : N) =
  (↑(r • x) : N)
Tactic: have eq1 : r • _ = (r • x).1 := congr_arg (r • ·) x.2.choose_spec
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (hypothesis)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst_7 : Fact (Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑i : (a : M) → N))
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)
⊢ (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)
have eq1₁ : Eq.{u_2 + 1} (α := N) ((i : (a : M) → N) (r • Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) sorry) : N)
  ((i : (a : M) → N) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑(r • x) : N)) sorry) : N)
Tactic: rw [← map_smul, ← (r • x).2.choose_spec] at eq1
Cleared hypotheses: eq1
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst_7 : Fact (Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑i : (a : M) → N))
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)
⊢ (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)
have dsimp : (f : (a : M) → Q) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = r • (↑x : N)) sorry) =
  HSMul.hSMul (β := Q) r ((f : (a : M) → Q) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) sorry) : Q)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst_7 : Fact (Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑i : (a : M) → N))
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)
⊢ (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)
have rw : (f : (a : M) → Q) (r • Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) sorry) =
  HSMul.hSMul (β := Q) r ((f : (a : M) → Q) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) sorry) : Q)
Tactic: rw [← Fact.out (p := Function.Injective i) eq1, map_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst_7 : Fact (Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑i : (a : M) → N))
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)
⊢ (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)
have rw₁ : HSMul.hSMul (β := Q) r ((f : (a : M) → Q) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) sorry) : Q) =
  HSMul.hSMul (β := Q) r ((f : (a : M) → Q) (Exists.choose (p := fun (y : M) ↦ (i : (a : M) → N) y = (↑x : N)) sorry) : Q)
Tactic: rw [← Fact.out (p := Function.Injective i) eq1, map_smul]