awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p : Submodule R M
p₂ : Submodule R₂ M₂
p₃ : Submodule R₃ M₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
hf : MapsTo (⇑f : (a : M) → M₂) (↑p : Set M) (↑p₂ : Set M₂)
hg : MapsTo (⇑g : (a : M₂) → M₃) (↑p₂ : Set M₂) (↑p₃ : Set M₃)
hfg : MapsTo (⇑(g ∘ₛₗ f) : (a : M) → M₃) (↑p : Set M) (↑p₃ : Set M₃)
⊢ (g ∘ₛₗ f).restrict hfg = g.restrict hg ∘ₛₗ f.restrict hf

Tactic:
rfl

Premises used: LinearMap.restrict, LinearMap.codRestrict, rfl
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_10
M : Type u_11
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
μ : R
h : ∀ x ∈ p, Membership.mem (α := M) p ((HSMul.hSMul (β := Module.End R M) μ 1 : (a : M) → M) x : M)
⊢ restrict (HSMul.hSMul (β := Module.End R M) μ 1) h = HSMul.hSMul (β := Module.End R ↥p) μ 1

Tactic:
rfl

Premises used: LinearMap.restrict, LinearMap.codRestrict, rfl
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : M →ₗ[R] M
h : Commute f g
p : Submodule R M
hf : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
hg : MapsTo (⇑g : (a : M) → M) (↑p : Set M) (↑p : Set M)
change : (f ∘ₗ g).restrict ⋯ = (g ∘ₗ f).restrict ⋯
⊢ Commute (f.restrict hf) (g.restrict hg)

Tactic:
change (f ∘ₗ g).restrict (hf.comp hg) = (g ∘ₗ f).restrict (hg.comp hf)

Premises used: LinearMap.restrict, LinearMap.comp, Set.MapsTo.comp
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : M →ₗ[R] M
h : Commute f g
p : Submodule R M
hf : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
hg : MapsTo (⇑g : (a : M) → M) (↑p : Set M) (↑p : Set M)
⊢ (f ∘ₗ g).restrict ⋯ = (g ∘ₗ f).restrict ⋯

Tactic:
congr 1
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
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₂
p : Submodule R M
q : Submodule R₂ M₂
hf : ∀ x ∈ p, Membership.mem (α := M₂) q ((f : (a : M) → M₂) x : M₂)
⊢ q.subtype ∘ₛₗ f.restrict hf = f.domRestrict p

Tactic:
rfl

Premises used: LinearMap.domRestrict, Submodule.subtype, rfl
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
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₂
p : Submodule R M
q : Submodule R₂ M₂
hf : ∀ x ∈ p, Membership.mem (α := M₂) q ((f : (a : M) → M₂) x : M₂)
⊢ f.restrict hf = codRestrict q (f.domRestrict p) ⋯

Tactic:
rfl

Premises used: LinearMap.restrict, rfl
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
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₂
p : Submodule R M
q : Submodule R₂ M₂
hf : ∀ (x : M), Membership.mem (α := M₂) q ((f : (a : M) → M₂) x : M₂)
⊢ f.restrict ⋯ = (codRestrict q f hf).domRestrict p

Tactic:
rfl

Premises used: LinearMap.restrict, LinearMap.domRestrict, LinearMap.codRestrict, rfl
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
ι : Type u_9
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₂
t : Finset ι
f : ι → M →ₛₗ[σ₁₂] M₂
b : M
⊢ Eq.{u_7 + 1} (α := M₂) ((∑ d ∈ t, f d : (a : M) → M₂) b : M₂) (∑ d ∈ t, (f d : (a : M) → M₂) b : M₂)

Tactic:
_root_.map_sum ((AddMonoidHom.eval b).comp toAddMonoidHom') f _

Premises used: AddMonoidHom.eval, LinearMap.toAddMonoidHom', map_sum, AddMonoidHom.comp, DFunLike.coe
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
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₂
ι : Type u_10
t : Finset ι
f : ι → M →ₛₗ[σ₁₂] M₂
⊢ Eq (α := (a : M) → M₂) (⇑(∑ i ∈ t, f i) : (a : M) → M₂) (∑ i ∈ t, (⇑(f i) : (a : M) → M₂))

Tactic:
_root_.map_sum
    (show AddMonoidHom (M →ₛₗ[σ₁₂] M₂) (M → M₂)
      from { toFun := DFunLike.coe,
             map_zero' := rfl
             map_add' := fun _ _ => rfl }) _ _

Premises used: AddMonoidHom.mk, map_sum, ZeroHom.mk, DFunLike.coe, rfl
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
g : Module.End R ↥N
G : Module.End R M
h : G ∘ₗ N.subtype = N.subtype ∘ₗ g
k : ℕ
hG : G ^ k = 0
h₁ : ∀ (m : ↥N), Eq.{u_5 + 1} (α := M) (↑((g ^ k : (a : ↥N) → ↥N) m) : M) (↑((0 : (a : ↥N) → ↥N) m) : M)
⊢ g ^ k = 0

Tactic:
ext m
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
g : Module.End R ↥N
G : Module.End R M
h : G ∘ₗ N.subtype = N.subtype ∘ₗ g
k : ℕ
hG : G ^ k = 0
m : ↥N
rw : Eq (α := M) (((G ^ k) ∘ₗ N.subtype : (a : ↥N) → M) m : M) (0 : M)
rw₁ : Eq (α := M) ((0 ∘ₗ N.subtype : (a : ↥N) → M) m : M) (0 : M)
rw₂ : Eq (α := M) ((0 : (a : ↥N) → M) m : M) (0 : M)
rw₃ rw₄ : Eq.{u_5 + 1} (α := M) 0 0
⊢ Eq (α := M) ((N.subtype ∘ₗ g ^ k : (a : ↥N) → M) m : M) (0 : M)

Tactic:
rw [← Module.End.commute_pow_left_of_commute h, hG, zero_comp, zero_apply]

Premises used: LinearMap.zero_apply, Module.End.commute_pow_left_of_commute, LinearMap.zero_comp
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
g : Module.End R ↥N
G : Module.End R M
h : G ∘ₗ N.subtype = N.subtype ∘ₗ g
k : ℕ
hG : G ^ k = 0
m : ↥N
⊢ Eq (α := M) ((N.subtype ∘ₗ g ^ k : (a : ↥N) → M) m : M) (0 : M)

Tactic:
have hg : N.subtype.comp (g ^ k) m = 0 := by
    rw [← Module.End.commute_pow_left_of_commute h, hG, zero_comp, zero_apply]
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
g : Module.End R ↥N
G : Module.End R M
h : G ∘ₗ N.subtype = N.subtype ∘ₗ g
k : ℕ
hG : G ^ k = 0
m : ↥N
hg : Eq (α := M) ((N.subtype ∘ₗ g ^ k : (a : ↥N) → M) m : M) (0 : M)
⊢ Eq.{u_5 + 1} (α := M) (↑((g ^ k : (a : ↥N) → ↥N) m) : M) (↑((0 : (a : ↥N) → ↥N) m) : M)

Tactic:
simpa using hg
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : M →ₗ[R] M
p : Submodule R M
h : ∀ x ∈ p, Membership.mem (α := M) p ((f' : (a : M) → M) x : M)
x : M
hx : x ∈ p
⊢ Membership.mem (α := M) p ((HPow.hPow (β := ℕ) f' 0 : (a : M) → M) x : M)

Tactic:
simpa
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : M →ₗ[R] M
p : Submodule R M
h : ∀ x ∈ p, Membership.mem (α := M) p ((f' : (a : M) → M) x : M)
n : ℕ
ih : ∀ (x : M) (hx : x ∈ p), Membership.mem (α := M) p ((f' ^ n : (a : M) → M) x : M)
x : M
hx : x ∈ p
⊢ Membership.mem (α := M) p ((f' ^ (n + 1) : (a : M) → M) x : M)

Tactic:
simpa only [iterate_succ, coe_comp, Function.comp_apply, restrict_apply] using ih _ (h _ hx)

Premises used: Function.iterate_succ, LinearMap.coe_comp, Function.comp_apply, LinearMap.restrict_apply
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : M →ₗ[R] M
p : Submodule R M
n : ℕ
h : ∀ x ∈ p, Membership.mem (α := M) p ((f' : (a : M) → M) x : M)
x : M
hx : x ∈ p
zero : ∀ (x : M) (hx : x ∈ p), Membership.mem (α := M) p ((HPow.hPow (β := ℕ) f' 0 : (a : M) → M) x : M)
succ :
  ∀ (n : ℕ) (ih : ∀ (x : M) (hx : x ∈ p), Membership.mem (α := M) p ((f' ^ n : (a : M) → M) x : M)) (x : M)
    (hx : x ∈ p), Membership.mem (α := M) p ((f' ^ (n + 1) : (a : M) → M) x : M)
⊢ Membership.mem (α := M) p ((f' ^ n : (a : M) → M) x : M)

Tactic:
induction n generalizing x with
  | zero => simpa
  | succ n ih =>
    simpa only [iterate_succ, coe_comp, Function.comp_apply, restrict_apply] using ih _ (h _ hx)

Premises used: Function.iterate_succ, LinearMap.coe_comp, Function.comp_apply, LinearMap.restrict_apply
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : M →ₗ[R] M
p : Submodule R M
n : ℕ
h : ∀ x ∈ p, Membership.mem (α := M) p ((f' : (a : M) → M) x : M)
h' : ∀ (x : M) (hx : x ∈ p), Membership.mem (α := M) p ((f' ^ n : (a : M) → M) x : M)
h₁ :
  ∀ (x : ↥p),
    Eq.{u_5 + 1} (α := M) (↑((f'.restrict h ^ n : (a : ↥p) → ↥p) x) : M)
      (↑(((f' ^ n).restrict h' : (a : ↥p) → ↥p) x) : M)
⊢ f'.restrict h ^ n = (f' ^ n).restrict h'

Tactic:
ext x
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : M →ₗ[R] M
p : Submodule R M
n : ℕ
h : ∀ x ∈ p, Membership.mem (α := M) p ((f' : (a : M) → M) x : M)
h' : ∀ (x : M) (hx : x ∈ p), Membership.mem (α := M) p ((f' ^ n : (a : M) → M) x : M)
x : ↥p
⊢ Semiconj (α := ↥p) (Subtype.val (p := fun (x : M) ↦ x ∈ p)) (⇑(f'.restrict h) : (a : ↥p) → ↥p) (⇑f' : (a : M) → M)

Tactic:
have : Semiconj (↑) (f'.restrict h) f' := fun _ ↦ coe_restrict_apply _ _
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : M →ₗ[R] M
p : Submodule R M
n : ℕ
h : ∀ x ∈ p, Membership.mem (α := M) p ((f' : (a : M) → M) x : M)
h' : ∀ (x : M) (hx : x ∈ p), Membership.mem (α := M) p ((f' ^ n : (a : M) → M) x : M)
x : ↥p
this :
  Semiconj (α := ↥p) (Subtype.val (p := fun (x : M) ↦ x ∈ p)) (⇑(f'.restrict h) : (a : ↥p) → ↥p) (⇑f' : (a : M) → M)
⊢ Eq.{u_5 + 1} (α := M) (↑((f'.restrict h ^ n : (a : ↥p) → ↥p) x) : M) (↑(((f' ^ n).restrict h' : (a : ↥p) → ↥p) x) : M)

Tactic:
simp [Module.End.coe_pow, this.iterate_right _ _]

Premises used: Module.End.coe_pow, Function.Semiconj.iterate_right
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
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
ι : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
f g : M →ₗ[R] M₂
p : Submodule R M
⊢ ∀ (x y : M →ₗ[R] M₂), (x + y).domRestrict p = x.domRestrict p + y.domRestrict p

Tactic:
simp [LinearMap.ext_iff]

Premises used: LinearMap.ext_iff
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
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
ι : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
f g : M →ₗ[R] M₂
p : Submodule R M
⊢ ∀ (m : R) (x : M →ₗ[R] M₂),
    (m • x).domRestrict p = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R) (x.domRestrict p)

Tactic:
simp [LinearMap.ext_iff]

Premises used: LinearMap.ext_iff
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
M : Type u_5
M₂ : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
f : M →ₗ[R] M₂
p : Submodule R M
x : ↥p
⊢ Eq.{u_7 + 1} (α := M₂)
    ((((domRestrict' p : (a : M →ₗ[R] M₂) → ↥p →ₗ[R] M₂) f : LinearMap.{u_1, u_1, u_5, u_7} (RingHom.id R) (↥p) M₂) :
          (a : ↥p) → M₂)
        x :
      M₂)
    ((f : (a : M) → M₂) (↑x : M) : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p p' : Submodule R M
h : p ≤ p'
x : ↥p
⊢ (↑((inclusion h : (a : ↥p) → ↥p') x) : M) = (↑x : M)

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p p' : Submodule R M
h : p ≤ p'
x : ↥p
⊢ (inclusion h : (a : ↥p) → ↥p') x = Subtype.mk (p := fun (x : M) ↦ x ∈ p') (↑x : M) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p p' : Submodule R M
h : p ≤ p'
⊢ Injective (α := ↥p) (β := ↥p') (⇑(inclusion h) : (a : ↥p) → ↥p')

Tactic:
fun _ _ h =>
  Subtype.val_injective (Subtype.mk.inj h)

Premises used: Subtype.val_injective, Subtype.mk.inj, Function.Injective
-- Module: Mathlib.Algebra.Module.Submodule.LinearMap
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p q : Submodule R M
h : p ≤ q
⊢ q.subtype ∘ₗ inclusion h = p.subtype

Tactic:
rfl

Premises used: Set.Mem, Submodule.subtype, rfl
-- 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 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p_1 p' : Submodule R M
q q' : Submodule R₂ M₂
x : M
inst_10 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
p : Submodule R M
c : R₂
y : M
hy : y ∈ (↑p : Set M)
obtain :
  ∀ (a : R),
    Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M))
      (HSMul.hSMul.{u_3, u_7, u_7} (α := R₂) (β := M₂) ((σ₁₂ : (a : R) → R₂) a : R₂) ((f : (a : M) → M₂) y : M₂))
⊢ Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M))
    (HSMul.hSMul (β := M₂) c ((f : (a : M) → M₂) y : M₂))

Tactic:
obtain ⟨a, rfl⟩ := σ₁₂.surjective c

Premises used: RingHom.surjective, rfl
-- 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 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p_1 p' : Submodule R M
q q' : Submodule R₂ M₂
x : M
inst_10 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
p : Submodule R M
y : M
hy : y ∈ (↑p : Set M)
a : R
⊢ Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M))
    (HSMul.hSMul.{u_3, u_7, u_7} (α := R₂) (β := M₂) ((σ₁₂ : (a : R) → R₂) a : R₂) ((f : (a : M) → M₂) y : M₂))

Tactic:
⟨_, p.smul_mem a hy, map_smulₛₗ f _ _⟩

Premises used: Set.Mem, setOf, MulActionSemiHomClass.map_smulₛₗ, And.intro, Exists.intro, Set.image, Submodule.smul_mem
-- 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 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p_1 p' : Submodule R M
q q' : Submodule R₂ M₂
x : M
inst_10 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
p : Submodule R M
y : M
hy : y ∈ (↑p : Set M)
a : R
⊢ Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M))
    (HSMul.hSMul.{u_3, u_7, u_7} (α := R₂) (β := M₂) ((σ₁₂ : (a : R) → R₂) a : R₂) ((f : (a : M) → M₂) y : M₂))

Tactic:
exact ⟨_, p.smul_mem a hy, map_smulₛₗ f _ _⟩
-- 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
⊢ (↑(map f p) : Set M₂) = (⇑f : (a : M) → M₂) '' (↑p : Set M)

Tactic:
rfl

Premises used: setOf, Set.image, 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
⊢ (map f p).toAddSubmonoid = AddSubmonoid.map (F := M →+ M₂) (↑f : M →+ M₂) p.toAddSubmonoid

Tactic:
SetLike.coe_injective rfl

Premises used: SetLike.coe_injective, 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
⊢ (map f p).toAddSubmonoid = AddSubmonoid.map f p.toAddSubmonoid

Tactic:
SetLike.coe_injective rfl

Premises used: SetLike.coe_injective, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
A : Type u_9
A₂ : Type u_10
inst : AddCommGroup A
inst_1 : AddCommGroup A₂
f : A →+ A₂
s : AddSubgroup A
⊢ map f.toIntLinearMap ((AddSubgroup.toIntSubmodule : (a : AddSubgroup A) → Submodule ℤ A) s) =
    (AddSubgroup.toIntSubmodule : (a : AddSubgroup A₂) → Submodule ℤ A₂) (AddSubgroup.map f s)

Tactic:
rfl

Premises used: Submodule.map, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
G : Type u_9
G₂ : Type u_10
inst : Group G
inst_1 : Group G₂
f : G →* G₂
s : Subgroup G
⊢ Eq.{u_10 + 1} (α := AddSubgroup (Additive G₂))
    (AddSubgroup.map.{u_9, u_10} (G := Additive G)
      ((MonoidHom.toAdditive : (a : G →* G₂) → Additive G →+ Additive G₂) f)
      ((Subgroup.toAddSubgroup : (a : Subgroup G) → AddSubgroup (Additive G)) s))
    ((Subgroup.toAddSubgroup : (a : Subgroup G₂) → AddSubgroup (Additive G₂)) (Subgroup.map f s))

Tactic:
rfl

Premises used: Set.Mem, Additive, setOf, Set.preimage, Set.image, rfl, AddSubgroup.map
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
G : Type u_9
G₂ : Type u_10
inst : AddGroup G
inst_1 : AddGroup G₂
f : G →+ G₂
s : AddSubgroup G
⊢ Eq.{u_10 + 1} (α := Subgroup (Multiplicative G₂))
    (Subgroup.map.{u_9, u_10} (G := Multiplicative G)
      ((AddMonoidHom.toMultiplicative : (a : G →+ G₂) → Multiplicative G →* Multiplicative G₂) f)
      ((AddSubgroup.toSubgroup : (a : AddSubgroup G) → Subgroup (Multiplicative G)) s))
    ((AddSubgroup.toSubgroup : (a : AddSubgroup G₂) → Subgroup (Multiplicative G₂)) (AddSubgroup.map f s))

Tactic:
rfl

Premises used: Subgroup.map, Set.Mem, setOf, Multiplicative, Set.preimage, Set.image, 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
x : M₂
⊢ x ∈ map f p ↔ ∃ y ∈ p, (f : (a : M) → M₂) y = x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, 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 : 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
r : M
h : r ∈ p
⊢ Membership.mem (α := M₂) (map f p) ((f : (a : M) → M₂) r : M₂)

Tactic:
Set.mem_image_of_mem _ h

Premises used: Set.Mem, setOf, Set.mem_image_of_mem, 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 : 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
r : ↥p
⊢ Membership.mem (α := M₂) (map f p) ((f : (a : M) → M₂) (↑r : M) : M₂)

Tactic:
mem_map_of_mem r.prop

Premises used: Subtype.prop, Submodule.mem_map_of_mem
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
a : M
⊢ a ∈ map LinearMap.id p ↔ a ∈ p

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : RingHomSurjective σ₁₂
inst_11 : RingHomSurjective σ₂₃
inst_12 : RingHomSurjective σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
p : Submodule R M
⊢ (↑(map (g ∘ₛₗ f) p) : Set M₃) = (↑(map g (map f p)) : Set M₃)

Tactic:
simp only [← image_comp, map_coe, LinearMap.coe_comp, comp_apply]

Premises used: LinearMap.coe_comp, Set.image_comp, Function.comp_apply, Submodule.map_coe
-- 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 p' : Submodule R M
⊢ p ≤ p' → map f p ≤ map f p'

Tactic:
image_mono

Premises used: Set.Mem, Set.image_mono, setOf, 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 : 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
inst_6 : RingHomSurjective σ₁₂
this : ∃ (x : M), x ∈ p
⊢ ∀ (x : M₂), Membership.mem (γ := Submodule R₂ M₂) (map (σ₁₂ := σ₁₂) 0 p) x ↔ Membership.mem (γ := Submodule R₂ M₂) ⊥ x

Tactic:
simp [this, eq_comm]

Premises used: eq_comm
-- 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
inst_6 : RingHomSurjective σ₁₂
f g : M →ₛₗ[σ₁₂] M₂
m : M
hm : m ∈ (↑p : Set M)
⊢ Membership.mem (α := M₂) (map f p ⊔ map g p) ((f + g : (a : M) → M₂) m : M₂)

Tactic:
add_mem_sup (mem_map_of_mem hm) (mem_map_of_mem hm)

Premises used: Set.Mem, Submodule.add_mem_sup, Submodule.mem_map_of_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₂
p : Submodule R M
inst_6 : RingHomSurjective σ₁₂
f g : M →ₛₗ[σ₁₂] M₂
m : M
hm : m ∈ (↑p : Set M)
⊢ Membership.mem (α := M₂) (map f p ⊔ map g p) ((f + g : (a : M) → M₂) m : M₂)

Tactic:
exact add_mem_sup (mem_map_of_mem hm) (mem_map_of_mem hm)

Premises used: Submodule.add_mem_sup, Submodule.mem_map_of_mem