awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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 ⊥
⊢ Disjoint p q ↔ comap p.subtype q = ⊥
have rw₂ : Disjoint p q ↔ p ⊓ q = ⊥
Tactic: rw [← (map_injective_of_injective (show Injective p.subtype from Subtype.coe_injective)).eq_iff,
    map_comap_subtype, map_bot, disjoint_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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 = ⊥
⊢ Disjoint p q ↔ comap p.subtype q = ⊥
have rw₃ : p ⊓ q = ⊥ ↔ p ⊓ q = ⊥
Tactic: rw [← (map_injective_of_injective (show Injective p.subtype from Subtype.coe_injective)).eq_iff,
    map_comap_subtype, map_bot, disjoint_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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₂
⊢ comap (-f) p = comap f p
have h : ∀ (x : M), x ∈ comap (-f) p ↔ x ∈ comap f p
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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 = comap f p
have h₁ : ∀ (b : V), b ∈ comap (a • f) p ↔ b ∈ comap f p
Tactic: ext b
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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 ≤ map f p
have rw : p ≤ comap (a • f) (map f p)
Tactic: rw [map_le_iff_le_comap, comap_smul f _ a h, ← map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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)
⊢ map (a • f) p ≤ map f p
have rw₁ : p ≤ comap f (map f p)
Tactic: rw [map_le_iff_le_comap, comap_smul f _ a h, ← map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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)
⊢ map (a • f) p ≤ map f p
have rw₂ : map f p ≤ map f p
Tactic: rw [map_le_iff_le_comap, comap_smul f _ a h, ← map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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 f p ≤ map (a • f) p
have rw : p ≤ comap f (map (a • f) p)
Tactic: rw [map_le_iff_le_comap, ← comap_smul f _ a h, ← map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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)
⊢ map f p ≤ map (a • f) p
have rw₁ : p ≤ comap (a • f) (map (a • f) p)
Tactic: rw [map_le_iff_le_comap, ← comap_smul f _ a h, ← map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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)
⊢ map f p ≤ map (a • f) p
have rw₂ : map (a • f) p ≤ map (a • f) p
Tactic: rw [map_le_iff_le_comap, ← comap_smul f _ a h, ← map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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
⊢ comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p
have pos : ∀ (h : a = 0), comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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
⊢ comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p
have neg : ∀ (h : ¬a = 0), comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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
⊢ comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p
have pos : ∀ (h : a = 0), comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p
Tactic: classical by_cases h : a = 0 <;> simp [h, comap_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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
⊢ comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p
have neg : ∀ (h : ¬a = 0), comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p
Tactic: classical by_cases h : a = 0 <;> simp [h, comap_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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
⊢ map (a • f) p = ⨆ (_ : a ≠ 0), map f p
have pos : ∀ (h : a = 0), map (a • f) p = ⨆ (_ : a ≠ 0), map f p
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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
⊢ map (a • f) p = ⨆ (_ : a ≠ 0), map f p
have neg : ∀ (h : ¬a = 0), map (a • f) p = ⨆ (_ : a ≠ 0), map f p
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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
⊢ map (a • f) p = ⨆ (_ : a ≠ 0), map f p
have pos : ∀ (h : a = 0), map (a • f) p = ⨆ (_ : a ≠ 0), map f p
Tactic: classical by_cases h : a = 0 <;> simp [h, Submodule.map_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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
⊢ map (a • f) p = ⨆ (_ : a ≠ 0), map f p
have neg : ∀ (h : ¬a = 0), map (a • f) p = ⨆ (_ : a ≠ 0), map f p
Tactic: classical by_cases h : a = 0 <;> simp [h, Submodule.map_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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 ∈ p, ((↑e : M →ₛₗ[τ₁₂] M₂) : (a : M) → M₂) y = x) ↔ Membership.mem (α := M) p ((e.symm : (a : M₂) → M) x : M)
have mp : (∃ y ∈ p, ((↑e : M →ₛₗ[τ₁₂] M₂) : (a : M) → M₂) y = x) → Membership.mem (α := M) p ((e.symm : (a : M₂) → M) x : M)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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)
⊢ (∃ y ∈ p, ((↑e : M →ₛₗ[τ₁₂] M₂) : (a : M) → M₂) y = x) ↔ Membership.mem (α := M) p ((e.symm : (a : M₂) → M) x : M)
have mpr : Membership.mem (α := M) p ((e.symm : (a : M₂) → M) x : M) → ∃ y ∈ p, ((↑e : M →ₛₗ[τ₁₂] M₂) : (a : M) → M₂) y = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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₂
⊢ x ∈ map (↑e : M →ₛₗ[τ₁₂] M₂) K ↔ x ∈ comap (↑e.symm : M₂ →ₛₗ[τ₂₁] M) K
have rw : Membership.mem (α := M) K ((e.symm : (a : M₂) → M) x : M) ↔ x ∈ comap (↑e.symm : M₂ →ₛₗ[τ₂₁] M) K
Tactic: rw [mem_map_equiv, mem_comap, LinearEquiv.coe_coe]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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
⊢ x ∈ map (↑e : M →ₛₗ[τ₁₂] M₂) K ↔ x ∈ comap (↑e.symm : M₂ →ₛₗ[τ₂₁] M) K
have 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)
Tactic: rw [mem_map_equiv, mem_comap, LinearEquiv.coe_coe]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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)
⊢ x ∈ map (↑e : M →ₛₗ[τ₁₂] M₂) K ↔ x ∈ comap (↑e.symm : M₂ →ₛₗ[τ₂₁] M) K
have rw₂ : Membership.mem (α := M) K ((e.symm : (a : M₂) → M) x : M) ↔ Membership.mem (α := M) K ((e.symm : (a : M₂) → M) x : M)
Tactic: rw [mem_map_equiv, mem_comap, LinearEquiv.coe_coe]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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₂
⊢ map (↑e.symm : M₂ →ₛₗ[τ₂₁] M) K = p ↔ map (↑e : M →ₛₗ[τ₁₂] M₂) p = K
have rw : comap (↑e.symm.symm : M →ₛₗ[τ₁₂] M₂) K = p ↔ map (↑e : M →ₛₗ[τ₁₂] M₂) p = K
Tactic: rw [map_equiv_eq_comap_symm]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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₂
⊢ comap f₁ q ⊓ comap f₂ q ≤ comap (f₁ + f₂) q
have 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
Tactic: simp only [SetLike.le_def, mem_comap, mem_inf, LinearMap.add_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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₂
⊢ comap f q ≤ comap (c • f) q
have simp : ∀ ⦃x : M⦄,
  Membership.mem (α := M₂) q ((f : (a : M) → M₂) x : M₂) → HSMul.hSMul (β := M₂) c ((f : (a : M) → M₂) x : M₂) ∈ q
Tactic: simp only [SetLike.le_def, mem_comap, LinearMap.smul_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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₂
⊢ map (c • f) p ≤ map f p
have grw : p ≤ comap (c • f) (map f p)
Tactic: grw [map_le_iff_le_comap, ← comap_le_comap_smul (map f p) f c, ← map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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)
⊢ map (c • f) p ≤ map f p
have grw₁ : p ≤ comap f (map f p)
Tactic: grw [map_le_iff_le_comap, ← comap_le_comap_smul (map f p) f c, ← map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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)
⊢ map (c • f) p ≤ map f p
have grw₂ : map 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]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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₂
⊢ Membership.mem (γ := Set (N →ₗ[S] N₂)) {fₗ : N →ₗ[S] N₂ | pₗ ≤ comap fₗ qₗ} (f₁ + f₂)
have apply : pₗ ≤ comap f₁ qₗ ⊓ comap f₂ qₗ
Tactic: apply le_trans _ (inf_comap_le_comap_add qₗ f₁ f₂)
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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ₗ ⊓ comap f₂ qₗ
have rw : pₗ ≤ comap f₁ qₗ ∧ pₗ ≤ comap f₂ qₗ
Tactic: rw [le_inf_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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
⊢ ∃ (a : ↥(Submodule.comap f q)), (f.submoduleComap q : (a : ↥(Submodule.comap f q)) → ↥q) a = y
have 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
Tactic: obtain ⟨x, hx⟩ := hf y
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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₂)
⊢ ∃ (a : ↥(Submodule.comap f q)), (f.submoduleComap q : (a : ↥(Submodule.comap f q)) → ↥q) a = y
have h : (f.submoduleComap q : (a : ↥(Submodule.comap f q)) → ↥q) (Subtype.mk (p := fun (x : M) ↦ x ∈ Submodule.comap f q) x sorry) =
  y
Tactic: use ⟨x, Submodule.mem_comap.mpr (hx ▸ y.2)⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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 ⋯) =
    y
have h : (↑((f.submoduleComap q : (a : ↥(Submodule.comap f q)) → ↥q)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ Submodule.comap f q) x sorry)) :
    M₂) =
  (↑y : M₂)
Tactic: apply Subtype.val_injective
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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
⊢ map (f.restrict h) p' = comap q.subtype (map f (map p.subtype p'))
have rw : map (codRestrict q (f.domRestrict p) sorry) p' = comap q.subtype (map f (map p.subtype p'))
Tactic: rw [restrict_eq_codRestrict_domRestrict, map_codRestrict, map_domRestrict]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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'))
⊢ map (f.restrict h) p' = comap q.subtype (map f (map p.subtype p'))
have rw₁ : comap q.subtype (map (f.domRestrict p) p') = comap q.subtype (map f (map p.subtype p'))
Tactic: rw [restrict_eq_codRestrict_domRestrict, map_codRestrict, map_domRestrict]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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'))
⊢ map (f.restrict h) p' = comap q.subtype (map f (map p.subtype p'))
have rw₂ : comap q.subtype (map f (map p.subtype p')) = comap q.subtype (map f (map p.subtype p'))
Tactic: rw [restrict_eq_codRestrict_domRestrict, map_codRestrict, map_domRestrict]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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
⊢ comap (f.restrict h) p' = comap p.subtype (comap f (map q.subtype p'))
have rw : comap (codRestrict q (f.domRestrict p) sorry) p' = comap p.subtype (comap f (map q.subtype p'))
Tactic: rw [restrict_eq_codRestrict_domRestrict, comap_codRestrict, comap_domRestrict]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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'))
⊢ comap (f.restrict h) p' = comap p.subtype (comap f (map q.subtype p'))
have rw₁ : comap (f.domRestrict p) (map q.subtype p') = comap p.subtype (comap f (map q.subtype p'))
Tactic: rw [restrict_eq_codRestrict_domRestrict, comap_codRestrict, comap_domRestrict]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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'))
⊢ comap (f.restrict h) p' = comap p.subtype (comap f (map q.subtype p'))
have rw₂ : comap p.subtype (comap f (map q.subtype p')) = comap p.subtype (comap f (map q.subtype p'))
Tactic: rw [restrict_eq_codRestrict_domRestrict, comap_codRestrict, comap_domRestrict]