awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
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₂
⊢ comap f ⊥ = ⊤ ↔ f = 0

Tactic:
ker_eq_top

Premises used: LinearMap.ker_eq_top, LinearMap.ker
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
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₂
⊢ comap f ⊥ = ⊤ ↔ f = 0

Tactic:
exact ker_eq_top

Premises used: LinearMap.ker_eq_top
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
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₂
rw : f.range = ⊥ ↔ f.range ≤ ⊥
rw₁ rw₂ : f.range = ⊥ ↔ f.range = ⊥
⊢ f.range = ⊥ ↔ f = 0

Tactic:
rw [← range_le_bot_iff, le_bot_iff]

Premises used: le_bot_iff, LinearMap.range_le_bot_iff
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
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 τ₁₂
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
h : g ∘ₛₗ f = 0
x : M₂
hx : x ∈ f.range
y : M
hy : (f : (a : M) → M₂) y = x
rw : Eq.{u_7 + 1} (α := M₃) ((g : (a : M₂) → M₃) ((f : (a : M) → M₂) y : M₂) : M₃) (0 : M₃)
rw₁ : Eq.{u_7 + 1} (α := M₃) ((g ∘ₛₗ f : (a : M) → M₃) y : M₃) (0 : M₃)
rw₂ : Eq.{u_7 + 1} (α := M₃) ((0 : (a : M) → M₃) y : M₃) (0 : M₃)
rw₃ rw₄ : Eq.{u_7 + 1} (α := M₃) 0 0
⊢ Eq.{u_7 + 1} (α := M₃) ((g : (a : M₂) → M₃) x : M₃) (0 : M₃)

Tactic:
rw [← hy, ← comp_apply, h, zero_apply]

Premises used: LinearMap.zero_apply, LinearMap.comp_apply
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
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 : f.range = ⊤
p p' : Submodule R₂ M₂
H : comap f p ≤ comap f p'
rwa : ∀ ⦃x : M₂⦄, x ∈ p → x ∈ p'
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (x : M),
    Membership.mem (α := M₂) p ((f : (a : M) → M₂) x : M₂) → Membership.mem (α := M₂) p' ((f : (a : M) → M₂) x : M₂)
⊢ p ≤ p'

Tactic:
rwa [SetLike.le_def, (range_eq_top.1 hf).forall]

Premises used: Function.Surjective.forall, SetLike.le_def, LinearMap.range_eq_top, Iff.mp
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
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 : f.range = ⊤
⊢ Injective (comap f)

Tactic:
fun _ _ h =>
  le_antisymm ((comap_le_comap_iff hf).1 (le_of_eq h)) ((comap_le_comap_iff hf).1 (ge_of_eq h))

Premises used: ge_of_eq, le_antisymm, Iff.mp, Function.Injective, le_of_eq, LinearMap.comap_le_comap_iff
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
inst : Semiring R
M : Type u_10
P : Type u_11
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
g : P →ₗ[R] M
h : f ∘ₗ g = id
x : M
hx : x ∈ f.ker
rw : HSub.hSub (β := M) x ((g : (a : P) → M) 0 : M) = x
rw₁ : x - 0 = x
rw₂ rw₃ : x = x
⊢ HSub.hSub (β := M) x ((g : (a : P) → M) ((f : (a : M) → P) x : P) : M) = x

Tactic:
rw [hx, map_zero, sub_zero]

Premises used: sub_zero, map_zero
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
inst : Semiring R
M : Type u_10
P : Type u_11
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
g : P →ₗ[R] M
h : f ∘ₗ g = id
rw : f ∘ₗ id - f ∘ₗ g ∘ₗ f = 0
rw₁ : f - f ∘ₗ g ∘ₗ f = 0
rw₂ : f - (f ∘ₗ g) ∘ₗ f = 0
rw₃ : f - id ∘ₗ f = 0
rw₄ : f - f = 0
rw₅ rw₆ : Eq (α := M →ₗ[R] P) 0 0
⊢ f ∘ₗ (id - g ∘ₗ f) = 0

Tactic:
rw [comp_sub, comp_id, ← comp_assoc, h, id_comp, sub_self]

Premises used: sub_self, LinearMap.comp_assoc, LinearMap.comp_sub, LinearMap.comp_id, LinearMap.id_comp
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
inst : Semiring R
M : Type u_10
P : Type u_11
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
g : P →ₗ[R] M
h : LeftInverse.{u_10 + 1, u_11 + 1} (α := M) (β := P) (⇑g : (a : P) → M) (⇑f : (a : M) → P)
x : M
⊢ Membership.mem (α := P) (f ∘ₗ g - id).ker ((f : (a : M) → P) x : P)

Tactic:
simp [h x]
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
inst : Semiring R
M : Type u_10
P : Type u_11
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
g : P →ₗ[R] M
h : LeftInverse.{u_10 + 1, u_11 + 1} (α := M) (β := P) (⇑g : (a : P) → M) (⇑f : (a : M) → P)
x : P
hx : x ∈ (f ∘ₗ g - id).ker
⊢ (f : (a : M) → P) ((g : (a : P) → M) x : M) = x

Tactic:
simpa [sub_eq_zero] using hx

Premises used: sub_eq_zero
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ f.range.toAddSubgroup = f.toAddMonoidHom.range

Tactic:
rfl

Premises used: AddMonoidHom.range, AddSubgroup.copy, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst_6 : RingHomSurjective τ₁₂
p : Submodule R M
mp : f.ker ≤ p → ∃ y ∈ f.range, Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)
mpr : (∃ y ∈ f.range, Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)) → f.ker ≤ p
⊢ f.ker ≤ p ↔ ∃ y ∈ f.range, Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)

Tactic:
constructor
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst_6 : RingHomSurjective τ₁₂
p : Submodule R M
h : f.ker ≤ p
h₁ : 0 ∈ f.range ∧ Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {0} ⊆ (↑p : Set M)
⊢ ∃ y ∈ f.range, Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)

Tactic:
use 0
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst_6 : RingHomSurjective τ₁₂
p : Submodule R M
h : f.ker ≤ p
⊢ Membership.mem (γ := Set M₂) (Set.range.{u_6, u_5 + 1} (ι := M) (⇑f : (a : M) → M₂)) 0 ∧
    Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {0} ⊆ (↑p : Set M)

Tactic:
⟨⟨0, map_zero f⟩, h⟩

Premises used: map_zero, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst_6 : RingHomSurjective τ₁₂
p : Submodule R M
h : f.ker ≤ p
⊢ Membership.mem (γ := Set M₂) (Set.range.{u_6, u_5 + 1} (ι := M) (⇑f : (a : M) → M₂)) 0 ∧
    Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {0} ⊆ (↑p : Set M)

Tactic:
exact ⟨⟨0, map_zero f⟩, h⟩
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst_6 : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : y ∈ f.range
h₂ : Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)
z : M
hz : z ∈ f.ker
⊢ Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) z : M₂) (0 : M₂)

Tactic:
simp only [mem_ker] at hz

Premises used: LinearMap.mem_ker
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst_6 : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : y ∈ f.range
h₂ : Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)
z : M
hz : Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) z : M₂) (0 : M₂)
mpr :
  ∀ (h₁ : ∃ (y_1 : M), (f : (a : M) → M₂) y_1 = y) (h₂ : Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M))
    ⦃z : M⦄ (hz : Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) z : M₂) (0 : M₂)), z ∈ p
⊢ z ∈ p

Tactic:
rw [← SetLike.mem_coe, coe_range, Set.mem_range] at h₁

Premises used: Set.mem_range, LinearMap.coe_range, SetLike.mem_coe
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst_6 : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : ∃ (y_1 : M), (f : (a : M) → M₂) y_1 = y
h₂ : Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)
z : M
hz : Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) z : M₂) (0 : M₂)
mpr : ∀ (x : M) (hx : (f : (a : M) → M₂) x = y), z ∈ p
⊢ z ∈ p

Tactic:
obtain ⟨x, hx⟩ := h₁
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst_6 : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)
z : M
hz : Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) z : M₂) (0 : M₂)
x : M
hx : (f : (a : M) → M₂) x = y
⊢ x ∈ p

Tactic:
have hx' : x ∈ p := h₂ hx
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst_6 : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)
z : M
hz : Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) z : M₂) (0 : M₂)
x : M
hx : (f : (a : M) → M₂) x = y
hx' : x ∈ p
a : Membership.mem (γ := Set M) (Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y}) (z + x)
⊢ z + x ∈ p

Tactic:
apply h₂
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst_6 : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)
z : M
hz : Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) z : M₂) (0 : M₂)
x : M
hx : (f : (a : M) → M₂) x = y
hx' : x ∈ p
⊢ Membership.mem (γ := Set M) (Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y}) (z + x)

Tactic:
simp [hx, hz]
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst_6 : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)
z : M
hz : Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) z : M₂) (0 : M₂)
x : M
hx : (f : (a : M) → M₂) x = y
hx' : x ∈ p
⊢ z + x ∈ p

Tactic:
have hxz : z + x ∈ p := by
      apply h₂
      simp [hx, hz]
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst_6 : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)
z : M
hz : Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) z : M₂) (0 : M₂)
x : M
hx : (f : (a : M) → M₂) x = y
hx' : x ∈ p
hxz : z + x ∈ p
this : z + x - x ∈ p
⊢ z ∈ p

Tactic:
simpa only [this, add_sub_cancel_right]

Premises used: add_sub_cancel_right
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst_6 : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)
z : M
hz : Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) z : M₂) (0 : M₂)
x : M
hx : (f : (a : M) → M₂) x = y
hx' : x ∈ p
hxz : z + x ∈ p
mpr : z + x - x ∈ p
⊢ z ∈ p

Tactic:
suffices z + x - x ∈ p by simpa only [this, add_sub_cancel_right]
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst_6 : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)
z : M
hz : Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) z : M₂) (0 : M₂)
x : M
hx : (f : (a : M) → M₂) x = y
hx' : x ∈ p
hxz : z + x ∈ p
⊢ z + x - x ∈ p

Tactic:
p.sub_mem hxz hx'

Premises used: Submodule.sub_mem
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst_6 : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)
z : M
hz : Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) z : M₂) (0 : M₂)
x : M
hx : (f : (a : M) → M₂) x = y
hx' : x ∈ p
hxz : z + x ∈ p
⊢ z + x - x ∈ p

Tactic:
exact p.sub_mem hxz hx'

Premises used: Submodule.sub_mem
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
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₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
c : R₂
⊢ (c • f).range ≤ f.range

Tactic:
simpa only [range_eq_map] using Submodule.map_smul_le_map _ _ _

Premises used: Submodule.map_smul_le_map, LinearMap.range_eq_map
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
K : Type u_4
V : Type u_8
V₂ : Type u_9
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₂
a : K
h : a ≠ 0
⊢ (a • f).range = f.range

Tactic:
simpa only [range_eq_map] using Submodule.map_smul f _ a h

Premises used: LinearMap.range_eq_map, Submodule.map_smul
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
K : Type u_4
V : Type u_8
V₂ : Type u_9
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₂
a : K
⊢ (a • f).range = ⨆ (_ : a ≠ 0), f.range

Tactic:
simpa only [range_eq_map] using Submodule.map_smul' f _ a

Premises used: Submodule.map_smul', LinearMap.range_eq_map
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
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₂
⊢ map f ⊤ = f.range

Tactic:
(range_eq_map f).symm

Premises used: LinearMap.range_eq_map, Eq.symm
-- Module: Mathlib.Algebra.Module.Submodule.Range
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
⊢ p.subtype.range = p

Tactic:
simpa using map_comap_subtype p ⊤

Premises used: Submodule.map_comap_subtype, Top.top
-- Module: Mathlib.Algebra.Module.Submodule.Range
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
p' : Submodule R ↥p
⊢ map p.subtype p' ≤ p

Tactic:
simpa using (map_le_range : map p.subtype p' ≤ range p.subtype)

Premises used: LinearMap.map_le_range
-- Module: Mathlib.Algebra.Module.Submodule.Range
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
⊢ map p.subtype ⊤ = p

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Range
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
rw rw₁ : p ≤ p' ↔ p ≤ p'
⊢ map p.subtype ⊤ ≤ p' ↔ p ≤ p'

Tactic:
rw [map_subtype_top]

Premises used: Submodule.map_subtype_top
-- Module: Mathlib.Algebra.Module.Submodule.Range
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
⊢ p.submoduleOf q = ⊤ ↔ q ≤ p

Tactic:
simp [submoduleOf]

Premises used: Submodule.submoduleOf
-- Module: Mathlib.Algebra.Module.Submodule.Range
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
⊢ comap p.subtype p = ⊤

Tactic:
comap_subtype_eq_top.2 le_rfl

Premises used: Iff.mpr, le_rfl, Submodule.comap_subtype_eq_top
-- Module: Mathlib.Algebra.Module.Submodule.Range
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
⊢ N.submoduleOf N = ⊤

Tactic:
comap_subtype_self _

Premises used: Submodule.comap_subtype_self, Submodule.submoduleOf
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N₁ N₂ N : Submodule R M
h₁ : N₁ ≤ N
h₂ : N₂ ≤ N
a : map N.subtype ((N₁ ⊔ N₂).submoduleOf N) = map N.subtype (N₁.submoduleOf N ⊔ N₂.submoduleOf N)
⊢ (N₁ ⊔ N₂).submoduleOf N = N₁.submoduleOf N ⊔ N₂.submoduleOf N

Tactic:
apply Submodule.map_injective_of_injective N.subtype_injective

Premises used: Submodule.subtype_injective, Submodule.map_injective_of_injective
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N₁ N₂ N : Submodule R M
h₁ : N₁ ≤ N
h₂ : N₂ ≤ N
a : N.subtype.range ⊓ (N₁ ⊔ N₂) = map N.subtype (comap N.subtype N₁ ⊔ comap N.subtype N₂)
⊢ map N.subtype ((N₁ ⊔ N₂).submoduleOf N) = map N.subtype (N₁.submoduleOf N ⊔ N₂.submoduleOf N)

Tactic:
simp only [submoduleOf, map_comap_eq]

Premises used: Submodule.map_comap_eq, Submodule.submoduleOf
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N₁ N₂ N : Submodule R M
h₁ : N₁ ≤ N
h₂ : N₂ ≤ N
⊢ N.subtype.range ⊓ (N₁ ⊔ N₂) = map N.subtype (comap N.subtype N₁ ⊔ comap N.subtype N₂)

Tactic:
simp_all
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p q r : Submodule R M
h : comap p.subtype q ≤ comap p.subtype r
⊢ p ⊓ q ≤ p ⊓ r

Tactic:
simpa using map_mono (f := p.subtype) h

Premises used: Submodule.map_mono
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p q r : Submodule R M
h : p ⊓ q ≤ p ⊓ r
⊢ comap p.subtype q ≤ comap p.subtype r

Tactic:
simpa using comap_mono (f := p.subtype) h

Premises used: Submodule.comap_mono
-- Module: Mathlib.Algebra.Module.Submodule.Range
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
h : p ≤ q
rw : map (inclusion h) ⊤ = comap q.subtype p
rw₁ : map (codRestrict q p.subtype ⋯) ⊤ = comap q.subtype p
rw₂ : comap q.subtype (map p.subtype ⊤) = comap q.subtype p
rw₃ : comap q.subtype p.subtype.range = comap q.subtype p
rw₄ rw₅ : comap q.subtype p = comap q.subtype p
⊢ (inclusion h).range = comap q.subtype p

Tactic:
rw [← map_top, inclusion, LinearMap.map_codRestrict, map_top, range_subtype]

Premises used: Submodule.map_top, Submodule.inclusion, LinearMap.map_codRestrict, Submodule.range_subtype
-- Module: Mathlib.Algebra.Module.Submodule.Range
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
h : p ≤ p'
⊢ map p'.subtype (inclusion h).range = p

Tactic:
simp [range_inclusion, map_comap_eq, h]

Premises used: Submodule.map_comap_eq, Submodule.range_inclusion
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
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₂
inst_6 : SMul R R₂
inst_7 : Module R₂ M
inst_8 : Module R M₂
inst_9 : IsScalarTower R R₂ M
inst_10 : IsScalarTower R R₂ M₂
f : M →ₗ[R₂] M₂
M' : Submodule R₂ M
⊢ Eq (α := Submodule R M₂) (restrictScalars R (map f M'))
    (map
      ((↑R :
          {S : Type u_2} →
            {M : Type u_5} →
              {M₂ : Type u_6} →
                [inst : Semiring R] →
                  [inst_11 : Semiring S] →
                    [inst_12 : AddCommMonoid M] →
                      [inst_13 : AddCommMonoid M₂] →
                        [inst_14 : Module R M] →
                          [inst_15 : Module R M₂] →
                            [inst_16 : Module S M] →
                              [inst_17 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        f)
      (restrictScalars R M'))

Tactic:
rfl

Premises used: Set.Mem, Submodule.restrictScalars, setOf, Set.image, Submodule.map, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
V₂ : 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₂
p : Submodule R M
τ₁₂ : R →+* R₂
p' : Submodule R ↥p
⊢ Injective (α := ↥p) (β := M) (⇑p.subtype : (a : ↥p) → M)

Tactic:
Subtype.val_injective

Premises used: Subtype.val_injective
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
V₂ : 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₂
p : Submodule R M
τ₁₂ : R →+* R₂
p' : Submodule R ↥p
⊢ Injective (α := ↥p) (β := M) (⇑p.subtype : (a : ↥p) → M)

Tactic:
exact Subtype.val_injective

Premises used: Subtype.val_injective