awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f₁ f₂ : M →ₛₗ[τ₁₂] M₂
simp :
  ∀ ⦃x : M⦄,
    Membership.mem (α := M₂) q ((f₁ : (a : M) → M₂) x : M₂) ∧ Membership.mem (α := M₂) q ((f₂ : (a : M) → M₂) x : M₂) →
      HAdd.hAdd (α := M₂) (β := M₂) ((f₁ : (a : M) → M₂) x : M₂) ((f₂ : (a : M) → M₂) x : M₂) ∈ q
⊢ comap f₁ q ⊓ comap f₂ q ≤ comap (f₁ + f₂) q

Tactic:
simp only [SetLike.le_def, mem_comap, mem_inf, LinearMap.add_apply]

Premises used: LinearMap.add_apply, Submodule.mem_comap, SetLike.le_def, Submodule.mem_inf
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f₁ f₂ : M →ₛₗ[τ₁₂] M₂
⊢ ∀ ⦃x : M⦄,
    Membership.mem (α := M₂) q ((f₁ : (a : M) → M₂) x : M₂) ∧ Membership.mem (α := M₂) q ((f₂ : (a : M) → M₂) x : M₂) →
      HAdd.hAdd (α := M₂) (β := M₂) ((f₁ : (a : M) → M₂) x : M₂) ((f₂ : (a : M) → M₂) x : M₂) ∈ q

Tactic:
fun _ h ↦ add_mem h.1 h.2

Premises used: And.right, And.left, AddMemClass.add_mem
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f₁ f₂ : M →ₛₗ[τ₁₂] M₂
⊢ ∀ ⦃x : M⦄,
    Membership.mem (α := M₂) q ((f₁ : (a : M) → M₂) x : M₂) ∧ Membership.mem (α := M₂) q ((f₂ : (a : M) → M₂) x : M₂) →
      HAdd.hAdd (α := M₂) (β := M₂) ((f₁ : (a : M) → M₂) x : M₂) ((f₂ : (a : M) → M₂) x : M₂) ∈ q

Tactic:
exact fun _ h ↦ add_mem h.1 h.2

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
q : Submodule R₂ M₂
⊢ SurjOn (⇑f : (a : M) → M₂) (↑p : Set M) (↑q : Set M₂) ↔ q ≤ map f p

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.SurjOn, Set.Subset, Set.image
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : CommSemiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
c : R₂
simp :
  ∀ ⦃x : M⦄,
    Membership.mem (α := M₂) q ((f : (a : M) → M₂) x : M₂) → HSMul.hSMul (β := M₂) c ((f : (a : M) → M₂) x : M₂) ∈ q
⊢ comap f q ≤ comap (c • f) q

Tactic:
simp only [SetLike.le_def, mem_comap, LinearMap.smul_apply]

Premises used: LinearMap.smul_apply, Submodule.mem_comap, SetLike.le_def
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : CommSemiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
c : R₂
⊢ ∀ ⦃x : M⦄,
    Membership.mem (α := M₂) q ((f : (a : M) → M₂) x : M₂) → HSMul.hSMul (β := M₂) c ((f : (a : M) → M₂) x : M₂) ∈ q

Tactic:
fun _ h ↦ smul_mem _ _ h

Premises used: Submodule.smul_mem
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : CommSemiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
c : R₂
⊢ ∀ ⦃x : M⦄,
    Membership.mem (α := M₂) q ((f : (a : M) → M₂) x : M₂) → HSMul.hSMul (β := M₂) c ((f : (a : M) → M₂) x : M₂) ∈ q

Tactic:
exact fun _ h ↦ smul_mem _ _ h

Premises used: Submodule.smul_mem
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : CommSemiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
p : Submodule R M
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
c : R₂
grw : p ≤ comap (c • f) (map f p)
grw₁ : p ≤ comap f (map f p)
grw₂ grw₃ : map f p ≤ map f p
⊢ map (c • f) p ≤ map f p

Tactic:
grw [map_le_iff_le_comap, ← comap_le_comap_smul (map f p) f c, ← map_le_iff_le_comap]

Premises used: Submodule.comap_le_comap_smul, Submodule.map, Submodule.map_le_iff_le_comap
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
S : Type u_9
N : Type u_10
N₂ : Type u_11
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : CommSemiring R₂
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : Module R M
inst_6 : Module R₂ M₂
inst_7 : AddCommMonoid N
inst_8 : AddCommMonoid N₂
inst_9 : Module S N
inst_10 : Module S N₂
τ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule S N
qₗ : Submodule S N₂
f₁ f₂ : N →ₗ[S] N₂
h₁ : Membership.mem (γ := Set (N →ₗ[S] N₂)) {fₗ : N →ₗ[S] N₂ | pₗ ≤ comap fₗ qₗ} f₁
h₂ : Membership.mem (γ := Set (N →ₗ[S] N₂)) {fₗ : N →ₗ[S] N₂ | pₗ ≤ comap fₗ qₗ} f₂
apply : pₗ ≤ comap f₁ qₗ ⊓ comap f₂ qₗ
⊢ Membership.mem (γ := Set (N →ₗ[S] N₂)) {fₗ : N →ₗ[S] N₂ | pₗ ≤ comap fₗ qₗ} (f₁ + f₂)

Tactic:
apply le_trans _ (inf_comap_le_comap_add qₗ f₁ f₂)

Premises used: Submodule.inf_comap_le_comap_add, le_trans
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
S : Type u_9
N : Type u_10
N₂ : Type u_11
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : CommSemiring R₂
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : Module R M
inst_6 : Module R₂ M₂
inst_7 : AddCommMonoid N
inst_8 : AddCommMonoid N₂
inst_9 : Module S N
inst_10 : Module S N₂
τ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule S N
qₗ : Submodule S N₂
f₁ f₂ : N →ₗ[S] N₂
h₁ : Membership.mem (γ := Set (N →ₗ[S] N₂)) {fₗ : N →ₗ[S] N₂ | pₗ ≤ comap fₗ qₗ} f₁
h₂ : Membership.mem (γ := Set (N →ₗ[S] N₂)) {fₗ : N →ₗ[S] N₂ | pₗ ≤ comap fₗ qₗ} f₂
rw : pₗ ≤ comap f₁ qₗ ∧ pₗ ≤ comap f₂ qₗ
⊢ pₗ ≤ comap f₁ qₗ ⊓ comap f₂ qₗ

Tactic:
rw [le_inf_iff]

Premises used: le_inf_iff
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
S : Type u_9
N : Type u_10
N₂ : Type u_11
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : CommSemiring R₂
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : Module R M
inst_6 : Module R₂ M₂
inst_7 : AddCommMonoid N
inst_8 : AddCommMonoid N₂
inst_9 : Module S N
inst_10 : Module S N₂
τ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule S N
qₗ : Submodule S N₂
f₁ f₂ : N →ₗ[S] N₂
h₁ : Membership.mem (γ := Set (N →ₗ[S] N₂)) {fₗ : N →ₗ[S] N₂ | pₗ ≤ comap fₗ qₗ} f₁
h₂ : Membership.mem (γ := Set (N →ₗ[S] N₂)) {fₗ : N →ₗ[S] N₂ | pₗ ≤ comap fₗ qₗ} f₂
⊢ pₗ ≤ comap f₁ qₗ ∧ pₗ ≤ comap f₂ qₗ

Tactic:
⟨h₁, h₂⟩

Premises used: And.intro
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
S : Type u_9
N : Type u_10
N₂ : Type u_11
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : CommSemiring R₂
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : Module R M
inst_6 : Module R₂ M₂
inst_7 : AddCommMonoid N
inst_8 : AddCommMonoid N₂
inst_9 : Module S N
inst_10 : Module S N₂
τ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule S N
qₗ : Submodule S N₂
f₁ f₂ : N →ₗ[S] N₂
h₁ : Membership.mem (γ := Set (N →ₗ[S] N₂)) {fₗ : N →ₗ[S] N₂ | pₗ ≤ comap fₗ qₗ} f₁
h₂ : Membership.mem (γ := Set (N →ₗ[S] N₂)) {fₗ : N →ₗ[S] N₂ | pₗ ≤ comap fₗ qₗ} f₂
⊢ pₗ ≤ comap f₁ qₗ ∧ pₗ ≤ comap f₂ qₗ

Tactic:
exact ⟨h₁, h₂⟩
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
S : Type u_9
N : Type u_10
N₂ : Type u_11
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : CommSemiring R₂
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : Module R M
inst_6 : Module R₂ M₂
inst_7 : AddCommMonoid N
inst_8 : AddCommMonoid N₂
inst_9 : Module S N
inst_10 : Module S N₂
τ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule S N
qₗ : Submodule S N₂
⊢ Membership.mem (γ := Set (N →ₗ[S] N₂)) {fₗ : N →ₗ[S] N₂ | pₗ ≤ comap fₗ qₗ} 0

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
S : Type u_9
N : Type u_10
N₂ : Type u_11
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : CommSemiring R₂
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : Module R M
inst_6 : Module R₂ M₂
inst_7 : AddCommMonoid N
inst_8 : AddCommMonoid N₂
inst_9 : Module S N
inst_10 : Module S N₂
τ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule S N
qₗ : Submodule S N₂
c : S
fₗ : N →ₗ[S] N₂
h : pₗ ≤ comap fₗ qₗ
⊢ Membership.mem (γ := Set (N →ₗ[S] N₂)) {fₗ : N →ₗ[S] N₂ | pₗ ≤ comap fₗ qₗ} (c • fₗ)

Tactic:
le_trans h (comap_le_comap_smul qₗ fₗ c)

Premises used: Submodule.comap_le_comap_smul, Set.Mem, setOf, le_trans
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
S : Type u_9
N : Type u_10
N₂ : Type u_11
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : CommSemiring R₂
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : Module R M
inst_6 : Module R₂ M₂
inst_7 : AddCommMonoid N
inst_8 : AddCommMonoid N₂
inst_9 : Module S N
inst_10 : Module S N₂
τ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule S N
qₗ : Submodule S N₂
c : S
fₗ : N →ₗ[S] N₂
h : pₗ ≤ comap fₗ qₗ
⊢ Membership.mem (γ := Set (N →ₗ[S] N₂)) {fₗ : N →ₗ[S] N₂ | pₗ ≤ comap fₗ qₗ} (c • fₗ)

Tactic:
exact le_trans h (comap_le_comap_smul qₗ fₗ c)

Premises used: Submodule.comap_le_comap_smul, le_trans
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
q : Submodule R₂ M₂
hf : Surjective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
y : ↥q
obtain :
  ∀ (x : M) (hx : (f : (a : M) → M₂) x = (↑y : M₂)),
    ∃ (a : ↥(Submodule.comap f q)), (f.submoduleComap q : (a : ↥(Submodule.comap f q)) → ↥q) a = y
⊢ ∃ (a : ↥(Submodule.comap f q)), (f.submoduleComap q : (a : ↥(Submodule.comap f q)) → ↥q) a = y

Tactic:
obtain ⟨x, hx⟩ := hf y

Premises used: Subtype.val
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
q : Submodule R₂ M₂
hf : Surjective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
y : ↥q
x : M
hx : (f : (a : M) → M₂) x = (↑y : M₂)
h :
  (f.submoduleComap q : (a : ↥(Submodule.comap f q)) → ↥q)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ Submodule.comap f q) x ⋯) =
    y
⊢ ∃ (a : ↥(Submodule.comap f q)), (f.submoduleComap q : (a : ↥(Submodule.comap f q)) → ↥q) a = y

Tactic:
use ⟨x, Submodule.mem_comap.mpr (hx ▸ y.2)⟩
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
q : Submodule R₂ M₂
hf : Surjective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
y : ↥q
x : M
hx : (f : (a : M) → M₂) x = (↑y : M₂)
h :
  (↑((f.submoduleComap q : (a : ↥(Submodule.comap f q)) → ↥q)
          (Subtype.mk (p := fun (x : M) ↦ x ∈ Submodule.comap f q) x ⋯)) :
      M₂) =
    (↑y : M₂)
⊢ (f.submoduleComap q : (a : ↥(Submodule.comap f q)) → ↥q)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ Submodule.comap f q) x ⋯) =
    y

Tactic:
apply Subtype.val_injective

Premises used: Subtype.val_injective
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
q : Submodule R₂ M₂
hf : Surjective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
y : ↥q
x : M
hx : (f : (a : M) → M₂) x = (↑y : M₂)
⊢ (↑((f.submoduleComap q : (a : ↥(Submodule.comap f q)) → ↥q)
          (Subtype.mk (p := fun (x : M) ↦ x ∈ Submodule.comap f q) x ⋯)) :
      M₂) =
    (↑y : M₂)

Tactic:
simp [hx]
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
p : Submodule R M
x : ↥p
⊢ Eq.{u_7 + 1} (α := M₂)
    ((↑(((f.submoduleMap p : LinearMap.{u_1, u_3, u_5, u_7} σ₁₂ ↥p ↥(Submodule.map f p)) :
              (a : ↥p) → ↥(Submodule.map f p))
            x) :
        M₂) :
      M₂)
    ((f : (a : M) → M₂) (↑x : M) : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
p : Submodule R M
⊢ Surjective.{u_5 + 1, u_7 + 1} (α := ↥p) (β := ↥(Submodule.map f p))
    (⇑(f.submoduleMap p) : (a : ↥p) → ↥(Submodule.map f p))

Tactic:
f.toAddMonoidHom.addSubmonoidMap_surjective _

Premises used: LinearMap.toAddMonoidHom, Set.Mem, AddMonoidHom.addSubmonoidMap_surjective
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p : Submodule R M
⊢ Injective.{u_5 + 1, u_7 + 1} (α := ↥p) (β := ↥(Submodule.map f p))
    (⇑(f.submoduleMap p) : (a : ↥p) → ↥(Submodule.map f p))

Tactic:
f.toAddMonoidHom.addSubmonoidMap_injective hf _

Premises used: AddMonoidHom.addSubmonoidMap_injective, Set.Mem
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₂₁ : R₂ →+* R
inst_6 : RingHomSurjective σ₂₁
p : Submodule R M
f : M₂ →ₛₗ[σ₂₁] M
h : ∀ (c : M₂), Membership.mem (α := M) p ((f : (a : M₂) → M) c : M)
p' : Submodule R₂ M₂
x_1 : ↥p
x : M
hx : x ∈ p
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx ∈ map (codRestrict p f h) p' ↔
    Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx ∈ comap p.subtype (map f p')

Tactic:
simp [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₂₁ : R₂ →+* R
p : Submodule R M
f : M₂ →ₛₗ[σ₂₁] M
hf : ∀ (c : M₂), Membership.mem (α := M) p ((f : (a : M₂) → M) c : M)
p' : Submodule R ↥p
x : M₂
property : f.toAddHom.1 x ∈ p
h : Subtype.mk (p := fun (x : M) ↦ x ∈ p) (f.toAddHom.1 x) property ∈ (↑p' : Set ↥p)
⊢ x ∈ comap (codRestrict p f hf) p'

Tactic:
h

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₂₁ : R₂ →+* R
p : Submodule R M
f : M₂ →ₛₗ[σ₂₁] M
hf : ∀ (c : M₂), Membership.mem (α := M) p ((f : (a : M₂) → M) c : M)
p' : Submodule R ↥p
x : M₂
property : f.toAddHom.1 x ∈ p
h : Subtype.mk (p := fun (x : M) ↦ x ∈ p) (f.toAddHom.1 x) property ∈ (↑p' : Set ↥p)
⊢ x ∈ comap (codRestrict p f hf) p'

Tactic:
exact h
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₂₁ : R₂ →+* R
inst_6 : RingHomSurjective σ₂₁
p : Submodule R₂ M₂
f : M₂ →ₛₗ[σ₂₁] M
p' : Submodule R₂ ↥p
⊢ map (f.domRestrict p) p' = map f (map p.subtype p')

Tactic:
map_comp p.subtype f p'

Premises used: Submodule.map_comp, LinearMap.domRestrict, Submodule.subtype
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₂₁ : R₂ →+* R
p : Submodule R₂ M₂
f : M₂ →ₛₗ[σ₂₁] M
p' : Submodule R M
⊢ comap (f.domRestrict p) p' = comap p.subtype (comap f p')

Tactic:
comap_comp p.subtype f p'

Premises used: LinearMap.domRestrict, Submodule.comap_comp, Submodule.subtype
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₂₁ : R₂ →+* R
inst_6 : RingHomSurjective σ₂₁
p : Submodule R₂ M₂
q : Submodule R M
f : M₂ →ₛₗ[σ₂₁] M
h : ∀ x ∈ p, Membership.mem (α := M) q ((f : (a : M₂) → M) x : M)
p' : Submodule R₂ ↥p
rw : map (codRestrict q (f.domRestrict p) ⋯) p' = comap q.subtype (map f (map p.subtype p'))
rw₁ : comap q.subtype (map (f.domRestrict p) p') = comap q.subtype (map f (map p.subtype p'))
rw₂ rw₃ : comap q.subtype (map f (map p.subtype p')) = comap q.subtype (map f (map p.subtype p'))
⊢ map (f.restrict h) p' = comap q.subtype (map f (map p.subtype p'))

Tactic:
rw [restrict_eq_codRestrict_domRestrict, map_codRestrict, map_domRestrict]

Premises used: LinearMap.restrict_eq_codRestrict_domRestrict, LinearMap.map_domRestrict, LinearMap.map_codRestrict
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₂₁ : R₂ →+* R
inst_6 : RingHomSurjective σ₂₁
p : Submodule R₂ M₂
q : Submodule R M
f : M₂ →ₛₗ[σ₂₁] M
h : ∀ x ∈ p, Membership.mem (α := M) q ((f : (a : M₂) → M) x : M)
p' : Submodule R ↥q
rw : comap (codRestrict q (f.domRestrict p) ⋯) p' = comap p.subtype (comap f (map q.subtype p'))
rw₁ : comap (f.domRestrict p) (map q.subtype p') = comap p.subtype (comap f (map q.subtype p'))
rw₂ rw₃ : comap p.subtype (comap f (map q.subtype p')) = comap p.subtype (comap f (map q.subtype p'))
⊢ comap (f.restrict h) p' = comap p.subtype (comap f (map q.subtype p'))

Tactic:
rw [restrict_eq_codRestrict_domRestrict, comap_codRestrict, comap_domRestrict]

Premises used: LinearMap.comap_domRestrict, LinearMap.restrict_eq_codRestrict_domRestrict, LinearMap.comap_codRestrict
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
x : ↥p
⊢ (↑x : M) ∈ (↑p : Set M) ∧
    Eq.{u_7 + 1} (α := M₂) (((↑e : M →ₛₗ[σ₁₂] M₂) : (a : M) → M₂) (↑x : M) : M₂)
      (((↑e : M →ₛₗ[σ₁₂] M₂).domRestrict p : (a : ↥p) → M₂) x : M₂)

Tactic:
simp only [LinearMap.domRestrict_apply, and_true, SetLike.coe_mem,
          SetLike.mem_coe]

Premises used: and_true, SetLike.coe_mem, SetLike.mem_coe, LinearMap.domRestrict_apply
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
y : ↥(Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p)
rcases :
  ∀ (y' : M₂) (hy : y' ∈ Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p),
    Membership.mem (α := M) p
      (((↑e.symm : M₂ →ₛₗ[σ₂₁] M) : (a : M₂) → M)
          (↑(Subtype.mk (p := fun (x : M₂) ↦ x ∈ Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p) y' hy) : M₂) :
        M)
⊢ Membership.mem (α := M) p (((↑e.symm : M₂ →ₛₗ[σ₂₁] M) : (a : M₂) → M) (↑y : M₂) : M)

Tactic:
rcases y with ⟨y', hy⟩
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
y' : M₂
hy : y' ∈ Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p
⊢ ∃ y ∈ p, ((↑e : M →ₛₗ[σ₁₂] M₂) : (a : M) → M₂) y = y'

Tactic:
rw [Submodule.mem_map] at hy

Premises used: Submodule.mem_map
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
y' : M₂
hy_1 : y' ∈ Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p
hy : ∃ y ∈ p, ((↑e : M →ₛₗ[σ₁₂] M₂) : (a : M) → M₂) y = y'
rcases :
  ∀ (x : M) (hx : x ∈ p) (hxy : ((↑e : M →ₛₗ[σ₁₂] M₂) : (a : M) → M₂) x = y'),
    Membership.mem (α := M) p
      (((↑e.symm : M₂ →ₛₗ[σ₂₁] M) : (a : M₂) → M)
          (↑(Subtype.mk (p := fun (x : M₂) ↦ x ∈ Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p) y' hy_1) : M₂) :
        M)
⊢ Membership.mem (α := M) p
    (((↑e.symm : M₂ →ₛₗ[σ₂₁] M) : (a : M₂) → M)
        (↑(Subtype.mk (p := fun (x : M₂) ↦ x ∈ Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p) y' hy_1) : M₂) :
      M)

Tactic:
rcases hy with ⟨x, hx, hxy⟩
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
y' : M₂
hy : y' ∈ Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p
x : M
hx : x ∈ p
hxy : ((↑e : M →ₛₗ[σ₁₂] M₂) : (a : M) → M₂) x = y'
subst :
  ∀
    (hy :
      Membership.mem (α := M₂) (Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p) (((↑e : M →ₛₗ[σ₁₂] M₂) : (a : M) → M₂) x : M₂)),
    Membership.mem (α := M) p
      (((↑e.symm : M₂ →ₛₗ[σ₂₁] M) : (a : M₂) → M)
          ((↑(Subtype.mk (p := fun (x : M₂) ↦ x ∈ Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p)
                  (((↑e : M →ₛₗ[σ₁₂] M₂) : (a : M) → M₂) x) hy) :
              M₂) :
            M₂) :
        M)
⊢ Membership.mem (α := M) p
    (((↑e.symm : M₂ →ₛₗ[σ₂₁] M) : (a : M₂) → M)
        (↑(Subtype.mk (p := fun (x : M₂) ↦ x ∈ Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p) y' hy) : M₂) :
      M)

Tactic:
subst hxy