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₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R M
h : p ⋖ q
P : Submodule R₂ M₂
h₁ : map f p < P
h₂ : P < map f q
⊢ P ≤ map f (comap f P)

Tactic:
(Set.image_preimage_eq_of_subset (.trans h₂.le (Set.image_subset_range _ _))).superset

Premises used: Set.Mem, setOf, HasSubset.Subset.trans, Set.image_subset_range, LT.lt.le, Set.Subset, Set.preimage, Set.image_preimage_eq_of_subset, Set.image, Eq.superset
-- 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 q : Submodule R M
h : p ⋖ q
P : Submodule R₂ M₂
h₁ : map f p < P
h₂ : P < map f q
⊢ P ≤ map f (comap f P)

Tactic:
exact (Set.image_preimage_eq_of_subset (.trans h₂.le (Set.image_subset_range _ _))).superset

Premises used: HasSubset.Subset.trans, Set.image_subset_range, LT.lt.le, Set.image_preimage_eq_of_subset, Eq.superset
-- 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 σ₁₂
σ₂₁ : R₂ →+* R
inst_7 : RingHomInvPair σ₁₂ σ₂₁
inst_8 : RingHomInvPair σ₂₁ σ₁₂
f : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R₂ M₂
⊢ ((orderIsoMapComap f).symm : (a : Submodule R₂ M₂) → Submodule R M) p = comap (↑f : M →ₛₗ[σ₁₂] M₂) p

Tactic:
rfl

Premises used: Submodule.comap, 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₂
p : Submodule R M
inst_6 : RingHomSurjective σ₁₂
σ₂₁ : R₂ →+* R
inst_7 : RingHomInvPair σ₁₂ σ₂₁
inst_8 : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
⊢ map (↑e : M →ₛₗ[σ₁₂] M₂) p = ⊥ ↔ p = ⊥

Tactic:
map_eq_bot_iff (orderIsoMapComap e)

Premises used: Submodule.orderIsoMapComap, map_eq_bot_iff, Submodule.map
-- 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 σ₁₂
σ₂₁ : R₂ →+* R
inst_7 : RingHomInvPair σ₁₂ σ₂₁
inst_8 : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
⊢ map (↑e : M →ₛₗ[σ₁₂] M₂) p = ⊤ ↔ p = ⊤

Tactic:
map_eq_top_iff (orderIsoMapComap e)

Premises used: map_eq_top_iff, Submodule.orderIsoMapComap, Submodule.map
-- 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 σ₁₂
σ₂₁ : R₂ →+* R
inst_7 : RingHomInvPair σ₁₂ σ₂₁
inst_8 : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
⊢ map (↑e : M →ₛₗ[σ₁₂] M₂) p ≠ ⊥ ↔ p ≠ ⊥

Tactic:
simp
-- 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 σ₁₂
σ₂₁ : R₂ →+* R
inst_7 : RingHomInvPair σ₁₂ σ₂₁
inst_8 : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
⊢ map (↑e : M →ₛₗ[σ₁₂] M₂) p ≠ ⊤ ↔ p ≠ ⊤

Tactic:
simp
-- 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
p' : Submodule R₂ M₂
x : M
h₁ : x ∈ (↑p : Set M)
h₂ : Membership.mem (α := M₂) (↑p' : Set M₂) ((f : (a : M) → M₂) x : M₂)
⊢ Membership.mem (α := M₂) (map f (p ⊓ comap f p')) ((f : (a : M) → M₂) x : M₂)

Tactic:
⟨_, ⟨h₁, h₂⟩, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, 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
p' : Submodule R₂ M₂
x : M
h₁ : x ∈ (↑p : Set M)
h₂ : Membership.mem (α := M₂) (↑p' : Set M₂) ((f : (a : M) → M₂) x : M₂)
⊢ Membership.mem (α := M₂) (map f (p ⊓ comap f p')) ((f : (a : M) → M₂) x : M₂)

Tactic:
exact ⟨_, ⟨h₁, h₂⟩, rfl⟩
-- 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 p' : Submodule R M
val : M
h₁ : val ∈ p
h₂ : Subtype.mk (p := fun (x : M) ↦ x ∈ p) val h₁ ∈ (↑(comap p.subtype p') : Set ↥p)
⊢ Membership.mem (α := M) (p ⊓ p') ((p.subtype : (a : ↥p) → M) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) val h₁) : M)

Tactic:
⟨h₁, h₂⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro
-- 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 p' : Submodule R M
val : M
h₁ : val ∈ p
h₂ : Subtype.mk (p := fun (x : M) ↦ x ∈ p) val h₁ ∈ (↑(comap p.subtype p') : Set ↥p)
⊢ Membership.mem (α := M) (p ⊓ p') ((p.subtype : (a : ↥p) → M) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) val h₁) : M)

Tactic:
exact ⟨h₁, h₂⟩
-- 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
σ : R →+* R
ι : Sort u_9
f : M →ₛₗ[σ] M
p : ι → Submodule R M
hf : ∀ (i : ι), ∀ v ∈ p i, Membership.mem (α := M) (p i) ((f : (a : M) → M) v : M)
simp : ∀ (v : M), (∀ (i : ι), v ∈ p i) → ∀ (i : ι), Membership.mem (α := M) (p i) ((f : (a : M) → M) v : M)
⊢ ∀ v ∈ iInf p, Membership.mem (α := M) (iInf p) ((f : (a : M) → M) v : M)

Tactic:
simp only [mem_iInf]

Premises used: Submodule.mem_iInf
-- 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
σ : R →+* R
ι : Sort u_9
f : M →ₛₗ[σ] M
p : ι → Submodule R M
hf : ∀ (i : ι), ∀ v ∈ p i, Membership.mem (α := M) (p i) ((f : (a : M) → M) v : M)
⊢ ∀ (v : M), (∀ (i : ι), v ∈ p i) → ∀ (i : ι), Membership.mem (α := M) (p i) ((f : (a : M) → M) v : M)

Tactic:
fun v a i ↦ hf i v (a i)
-- 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
σ : R →+* R
ι : Sort u_9
f : M →ₛₗ[σ] M
p : ι → Submodule R M
hf : ∀ (i : ι), ∀ v ∈ p i, Membership.mem (α := M) (p i) ((f : (a : M) → M) v : M)
⊢ ∀ (v : M), (∀ (i : ι), v ∈ p i) → ∀ (i : ι), Membership.mem (α := M) (p i) ((f : (a : M) → M) v : M)

Tactic:
exact fun v a i ↦ hf i v (a i)
-- 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 q : Submodule R M
rw : Disjoint p q ↔ map p.subtype (comap p.subtype q) = map p.subtype ⊥
rw₁ : Disjoint p q ↔ p ⊓ q = map p.subtype ⊥
rw₂ : Disjoint p q ↔ p ⊓ q = ⊥
rw₃ rw₄ : p ⊓ q = ⊥ ↔ p ⊓ q = ⊥
⊢ Disjoint p q ↔ comap p.subtype q = ⊥

Tactic:
rw [← (map_injective_of_injective (show Injective p.subtype from Subtype.coe_injective)).eq_iff,
    map_comap_subtype, map_bot, disjoint_iff]

Premises used: Function.Injective.eq_iff, Submodule.map_bot, disjoint_iff, Subtype.coe_injective, Submodule.map_comap_subtype, Submodule.map_injective_of_injective
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
M : Type u_5
M₂ : Type u_7
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
f : M →ₗ[R] M₂
⊢ map (-f) p = map f p

Tactic:
ext fun _ =>
    ⟨fun ⟨x, hx, hy⟩ => hy ▸ ⟨-x, show -x ∈ p from neg_mem hx, map_neg f x⟩, fun ⟨x, hx, hy⟩ =>
      hy ▸ ⟨-x, show -x ∈ p from neg_mem hx, (map_neg (-f) _).trans (neg_neg (f x))⟩⟩

Premises used: Membership.mem, Eq.rec, neg_neg, map_neg, And.intro, Iff.intro, Exists.intro, _private.0.Submodule.map_neg.match_2, Submodule.map, DFunLike.coe, _private.0.Submodule.map_neg.match_1, Submodule.ext, Neg.neg, Eq.trans, NegMemClass.neg_mem
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
M : Type u_5
M₂ : Type u_7
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
f : M →ₗ[R] M₂
p : Submodule R M₂
h : ∀ (x : M), x ∈ comap (-f) p ↔ x ∈ comap f p
⊢ comap (-f) p = comap f p

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
M : Type u_5
M₂ : Type u_7
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
f : M →ₗ[R] M₂
p : Submodule R M₂
x : M
⊢ x ∈ comap (-f) p ↔ x ∈ comap f p

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
R : Type u_1
M : Type u_5
M₂ : Type u_7
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
f : M →ₗ[R] M₂
p : Submodule R M
⊢ (map f p).toAddSubgroup = AddSubgroup.map (↑f : M →+ M₂) p.toAddSubgroup

Tactic:
rfl

Premises used: rfl, AddSubgroup.map
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : AddCommMonoid V₂
inst_4 : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V₂
a : K
h : a ≠ 0
h₁ : ∀ (b : V), b ∈ comap (a • f) p ↔ b ∈ comap f p
⊢ comap (a • f) p = comap f p

Tactic:
ext b
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : AddCommMonoid V₂
inst_4 : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V₂
a : K
h : a ≠ 0
b : V
⊢ b ∈ comap (a • f) p ↔ b ∈ comap f p

Tactic:
simp only [Submodule.mem_comap, p.smul_mem_iff h, LinearMap.smul_apply]

Premises used: LinearMap.smul_apply, Submodule.mem_comap, Submodule.smul_mem_iff
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : AddCommMonoid V₂
inst_4 : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V
a : K
h : a ≠ 0
rw : p ≤ comap (a • f) (map f p)
rw₁ : p ≤ comap f (map f p)
rw₂ rw₃ : map f p ≤ map f p
⊢ map (a • f) p ≤ map f p

Tactic:
rw [map_le_iff_le_comap, comap_smul f _ a h, ← map_le_iff_le_comap]

Premises used: Submodule.comap_smul, Submodule.map_le_iff_le_comap
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : AddCommMonoid V₂
inst_4 : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V
a : K
h : a ≠ 0
rw : p ≤ comap f (map (a • f) p)
rw₁ : p ≤ comap (a • f) (map (a • f) p)
rw₂ rw₃ : map (a • f) p ≤ map (a • f) p
⊢ map f p ≤ map (a • f) p

Tactic:
rw [map_le_iff_le_comap, ← comap_smul f _ a h, ← map_le_iff_le_comap]

Premises used: Submodule.comap_smul, Submodule.map_le_iff_le_comap
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : AddCommMonoid V₂
inst_4 : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V₂
a : K
pos : ∀ (h : a = 0), comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p
neg : ∀ (h : ¬a = 0), comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p
⊢ comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p

Tactic:
by_cases h : a = 0
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : AddCommMonoid V₂
inst_4 : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V₂
a : K
h : a = 0
⊢ comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p

Tactic:
simp [h, comap_smul]

Premises used: Submodule.comap_smul
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : AddCommMonoid V₂
inst_4 : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V₂
a : K
h : ¬a = 0
⊢ comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p

Tactic:
simp [h, comap_smul]

Premises used: Submodule.comap_smul
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : AddCommMonoid V₂
inst_4 : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V₂
a : K
pos : ∀ (h : a = 0), comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p
neg : ∀ (h : ¬a = 0), comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p
pos₁ : ∀ (h : a = 0), comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p
neg₁ : ∀ (h : ¬a = 0), comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p
pos₂ : ∀ (h : a = 0), comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p
neg₂ : ∀ (h : ¬a = 0), comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p
pos₃ : ∀ (h : a = 0), comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p
neg₃ : ∀ (h : ¬a = 0), comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p
⊢ comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p

Tactic:
classical by_cases h : a = 0 <;> simp [h, comap_smul]

Premises used: Submodule.comap_smul
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : AddCommMonoid V₂
inst_4 : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V
a : K
pos : ∀ (h : a = 0), map (a • f) p = ⨆ (_ : a ≠ 0), map f p
neg : ∀ (h : ¬a = 0), map (a • f) p = ⨆ (_ : a ≠ 0), map f p
⊢ map (a • f) p = ⨆ (_ : a ≠ 0), map f p

Tactic:
by_cases h : a = 0
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : AddCommMonoid V₂
inst_4 : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V
a : K
h : a = 0
⊢ map (a • f) p = ⨆ (_ : a ≠ 0), map f p

Tactic:
simp [h, Submodule.map_smul]

Premises used: Submodule.map_smul
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : AddCommMonoid V₂
inst_4 : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V
a : K
h : ¬a = 0
⊢ map (a • f) p = ⨆ (_ : a ≠ 0), map f p

Tactic:
simp [h, Submodule.map_smul]

Premises used: Submodule.map_smul
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : AddCommMonoid V₂
inst_4 : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V
a : K
pos : ∀ (h : a = 0), map (a • f) p = ⨆ (_ : a ≠ 0), map f p
neg : ∀ (h : ¬a = 0), map (a • f) p = ⨆ (_ : a ≠ 0), map f p
pos₁ : ∀ (h : a = 0), map (a • f) p = ⨆ (_ : a ≠ 0), map f p
neg₁ : ∀ (h : ¬a = 0), map (a • f) p = ⨆ (_ : a ≠ 0), map f p
pos₂ : ∀ (h : a = 0), map (a • f) p = ⨆ (_ : a ≠ 0), map f p
neg₂ : ∀ (h : ¬a = 0), map (a • f) p = ⨆ (_ : a ≠ 0), map f p
pos₃ : ∀ (h : a = 0), map (a • f) p = ⨆ (_ : a ≠ 0), map f p
neg₃ : ∀ (h : ¬a = 0), map (a • f) p = ⨆ (_ : a ≠ 0), map f p
⊢ map (a • f) p = ⨆ (_ : a ≠ 0), map f p

Tactic:
classical by_cases h : a = 0 <;> simp [h, Submodule.map_smul]

Premises used: Submodule.map_smul
-- 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 : AddCommMonoid M
inst_2 : Module R M
p q : Submodule R M
hpq : p ≤ q
x : ↥(comap q.subtype p)
⊢ (fun (x : ↥p) ↦
        (Subtype.mk (p := fun (x : ↥q) ↦ x ∈ comap q.subtype p) (Subtype.mk (p := fun (x : M) ↦ x ∈ q) (↑x : M) ⋯) ⋯ :
          ↥(comap q.subtype p)))
      ((fun (x : ↥(comap q.subtype p)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ p) (↑(↑x : ↥q) : M) ⋯) x) =
    x

Tactic:
simp only [SetLike.eta]

Premises used: SetLike.eta
-- 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 : AddCommMonoid M
inst_2 : Module R M
p q : Submodule R M
hpq : p ≤ q
x : ↥p
⊢ (fun (x : ↥(comap q.subtype p)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ p) (↑(↑x : ↥q) : M) ⋯)
      ((fun (x : ↥p) ↦
          (Subtype.mk (p := fun (x : ↥q) ↦ x ∈ comap q.subtype p) (Subtype.mk (p := fun (x : M) ↦ x ∈ q) (↑x : M) ⋯) ⋯ :
            ↥(comap q.subtype p)))
        x) =
    x

Tactic:
simp only [SetLike.eta]

Premises used: SetLike.eta
-- 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₂
τ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair τ₁₂ τ₂₁
inst_7 : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
mp : (∃ y ∈ p, ((↑e : M →ₛₗ[τ₁₂] M₂) : (a : M) → M₂) y = x) → Membership.mem (α := M) p ((e.symm : (a : M₂) → M) x : M)
mpr : Membership.mem (α := M) p ((e.symm : (a : M₂) → M) x : M) → ∃ y ∈ p, ((↑e : M →ₛₗ[τ₁₂] M₂) : (a : M) → M₂) y = x
⊢ (∃ y ∈ p, ((↑e : M →ₛₗ[τ₁₂] M₂) : (a : M) → M₂) y = x) ↔ Membership.mem (α := M) p ((e.symm : (a : M₂) → M) x : M)

Tactic:
constructor
-- 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₂
τ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair τ₁₂ τ₂₁
inst_7 : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
y : M
hy : y ∈ p
hx : ((↑e : M →ₛₗ[τ₁₂] M₂) : (a : M) → M₂) y = x
⊢ Membership.mem (α := M) p ((e.symm : (a : M₂) → M) x : M)

Tactic:
simp [← hx, hy]
-- 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₂
τ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair τ₁₂ τ₂₁
inst_7 : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
hx : Membership.mem (α := M) p ((e.symm : (a : M₂) → M) x : M)
⊢ ((↑e : M →ₛₗ[τ₁₂] M₂) : (a : M) → M₂) ((e.symm : (a : M₂) → M) x : M) = x

Tactic:
simp
-- 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₂
τ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair τ₁₂ τ₂₁
inst_7 : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
hx : Membership.mem (α := M) p ((e.symm : (a : M₂) → M) x : M)
⊢ ∃ y ∈ p, ((↑e : M →ₛₗ[τ₁₂] M₂) : (a : M) → M₂) y = x

Tactic:
exact ⟨e.symm x, hx, by simp⟩
-- 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₂
τ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair τ₁₂ τ₂₁
inst_7 : RingHomInvPair τ₂₁ τ₁₂
e : M ≃ₛₗ[τ₁₂] M₂
K : Submodule R M
x : M₂
rw : Membership.mem (α := M) K ((e.symm : (a : M₂) → M) x : M) ↔ x ∈ comap (↑e.symm : M₂ →ₛₗ[τ₂₁] M) K
rw₁ :
  Membership.mem (α := M) K ((e.symm : (a : M₂) → M) x : M) ↔
    Membership.mem (α := M) K (((↑e.symm : M₂ →ₛₗ[τ₂₁] M) : (a : M₂) → M) x : M)
rw₂ rw₃ :
  Membership.mem (α := M) K ((e.symm : (a : M₂) → M) x : M) ↔ Membership.mem (α := M) K ((e.symm : (a : M₂) → M) x : M)
⊢ x ∈ map (↑e : M →ₛₗ[τ₁₂] M₂) K ↔ x ∈ comap (↑e.symm : M₂ →ₛₗ[τ₂₁] M) K

Tactic:
rw [mem_map_equiv, mem_comap, LinearEquiv.coe_coe]

Premises used: Submodule.mem_comap, Submodule.mem_map_equiv, LinearEquiv.coe_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₂
τ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair τ₁₂ τ₂₁
inst_7 : RingHomInvPair τ₂₁ τ₁₂
e : M ≃ₛₗ[τ₁₂] M₂
K : Submodule R₂ M₂
⊢ comap (↑e : M →ₛₗ[τ₁₂] M₂) K = map (↑e.symm : M₂ →ₛₗ[τ₂₁] M) K

Tactic:
(map_equiv_eq_comap_symm e.symm K).symm

Premises used: LinearEquiv.symm, Submodule.map_equiv_eq_comap_symm, Eq.symm
-- 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₂
τ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair τ₁₂ τ₂₁
inst_7 : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
K : Submodule R₂ M₂
rw : comap (↑e.symm.symm : M →ₛₗ[τ₁₂] M₂) K = p ↔ map (↑e : M →ₛₗ[τ₁₂] M₂) p = K
⊢ map (↑e.symm : M₂ →ₛₗ[τ₂₁] M) K = p ↔ map (↑e : M →ₛₗ[τ₁₂] M₂) p = K

Tactic:
rw [map_equiv_eq_comap_symm]

Premises used: Submodule.map_equiv_eq_comap_symm
-- 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₂
τ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair τ₁₂ τ₂₁
inst_7 : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
K : Submodule R₂ M₂
⊢ comap (↑e.symm.symm : M →ₛₗ[τ₁₂] M₂) K = p ↔ map (↑e : M →ₛₗ[τ₁₂] M₂) p = K

Tactic:
(orderIsoMapComap e).symm_apply_eq.trans eq_comm

Premises used: OrderIso.symm_apply_eq, eq_comm, Submodule.orderIsoMapComap, Submodule.comap, Iff.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₂
τ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair τ₁₂ τ₂₁
inst_7 : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
K : Submodule R₂ M₂
⊢ comap (↑e.symm.symm : M →ₛₗ[τ₁₂] M₂) K = p ↔ map (↑e : M →ₛₗ[τ₁₂] M₂) p = K

Tactic:
exact (orderIsoMapComap e).symm_apply_eq.trans eq_comm

Premises used: OrderIso.symm_apply_eq, eq_comm, Submodule.orderIsoMapComap, Iff.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₂
τ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair τ₁₂ τ₂₁
inst_7 : RingHomInvPair τ₂₁ τ₁₂
e : M ≃ₛₗ[τ₁₂] M₂
p : Submodule R M
⊢ (orderIsoMapComap e : (a : Submodule R M) → Submodule R₂ M₂) p = comap (↑e.symm : M₂ →ₛₗ[τ₂₁] M) p

Tactic:
p.map_equiv_eq_comap_symm _

Premises used: Submodule.map_equiv_eq_comap_symm, Submodule.map
-- 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₂
τ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair τ₁₂ τ₂₁
inst_7 : RingHomInvPair τ₂₁ τ₁₂
e : M ≃ₛₗ[τ₁₂] M₂
p : Submodule R₂ M₂
⊢ ((orderIsoMapComap e).symm : (a : Submodule R₂ M₂) → Submodule R M) p = map (↑e.symm : M₂ →ₛₗ[τ₂₁] M) p

Tactic:
p.comap_equiv_eq_map_symm _

Premises used: Submodule.comap_equiv_eq_map_symm, Submodule.comap