awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
x y : M
hy : y ∈ (↑p : Set M)
e : Eq.{u_5 + 1} (α := M₂) ((f : (a : M) → M₂) y : M₂) ((f : (a : M) → M₂) x : M₂)
⊢ y + (x - y) = x

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
x y : M
hy : y ∈ (↑p : Set M)
e : Eq.{u_5 + 1} (α := M₂) ((f : (a : M) → M₂) y : M₂) ((f : (a : M) → M₂) x : M₂)
⊢ x ∈ p ⊔ f.ker

Tactic:
exact mem_sup.2 ⟨y, hy, x - y, by simpa using sub_eq_zero.2 e.symm, by simp⟩

Premises used: Iff.mpr, HSub.hSub, And.intro, Exists.intro, Submodule.mem_sup
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
p p' : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
hab : p ≤ p'
h : p ⊔ f.ker < p' ⊔ f.ker
⊢ comap f (map f p) < comap f (map f p')

Tactic:
simp_rw [← comap_map_eq] at h

Premises used: Submodule.comap_map_eq
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
p p' : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
hab : p ≤ p'
h : comap f (map f p) < comap f (map f p')
⊢ map f p < map f p'

Tactic:
lt_of_le_of_ne (map_mono hab) (ne_of_apply_ne _ h.ne)

Premises used: ne_of_apply_ne, Submodule.map_mono, lt_of_le_of_ne, LT.lt.ne
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
p p' : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
hab : p ≤ p'
h : comap f (map f p) < comap f (map f p')
⊢ map f p < map f p'

Tactic:
exact lt_of_le_of_ne (map_mono hab) (ne_of_apply_ne _ h.ne)

Premises used: ne_of_apply_ne, Submodule.map_mono, lt_of_le_of_ne, LT.lt.ne
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
h : f.ker ≤ p
rw : p ⊔ f.ker = p
rw₁ rw₂ : p = p
⊢ comap f (map f p) = p

Tactic:
rw [Submodule.comap_map_eq, sup_of_le_left h]

Premises used: sup_of_le_left, Submodule.comap_map_eq
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
q : Submodule R₂ M₂
le : comap f q ≤ p
⊢ comap f (map f p ⊔ q) = p

Tactic:
le_antisymm (fun x h ↦ ?_) (map_le_iff_le_comap.mp le_sup_left)

Premises used: le_sup_left, le_antisymm, Iff.mp, Submodule.map_le_iff_le_comap
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
q : Submodule R₂ M₂
le : comap f q ≤ p
refine : ∀ (x : M) (h : x ∈ comap f (map f p ⊔ q)), x ∈ p
⊢ comap f (map f p ⊔ q) = p

Tactic:
refine le_antisymm (fun x h ↦ ?_) (map_le_iff_le_comap.mp le_sup_left)

Premises used: le_sup_left, le_antisymm, Iff.mp, Submodule.map_le_iff_le_comap
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
q : Submodule R₂ M₂
le : comap f q ≤ p
x : M
h : x ∈ comap f (map f p ⊔ q)
obtain :
  ∀ (y : M) (hy : y ∈ (↑p : Set M)) (z : M₂) (hz : z ∈ q)
    (eq : HAdd.hAdd (α := M₂) ((f : (a : M) → M₂) y : M₂) z = (f : (a : M) → M₂) x), x ∈ p
⊢ x ∈ p

Tactic:
obtain ⟨_, ⟨y, hy, rfl⟩, z, hz, eq⟩ := mem_sup.mp h

Premises used: Iff.mp, Submodule.mem_sup, rfl
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
q : Submodule R₂ M₂
le : comap f q ≤ p
x : M
h : x ∈ comap f (map f p ⊔ q)
y : M
hy : y ∈ (↑p : Set M)
z : M₂
hz : z ∈ q
eq : HAdd.hAdd (α := M₂) ((f : (a : M) → M₂) y : M₂) z = (f : (a : M) → M₂) x
⊢ z = (f : (a : M) → M₂) (x - y)

Tactic:
rw [add_comm, ← eq_sub_iff_add_eq, ← map_sub] at eq

Premises used: map_sub, eq_sub_iff_add_eq, add_comm
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
q : Submodule R₂ M₂
le : comap f q ≤ p
x : M
h : x ∈ comap f (map f p ⊔ q)
y : M
hy : y ∈ (↑p : Set M)
z : M₂
hz : z ∈ q
eq : z = (f : (a : M) → M₂) (x - y)
⊢ Membership.mem (α := M₂) q ((f : (a : M) → M₂) (x - y) : M₂)

Tactic:
subst eq
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
q : Submodule R₂ M₂
le : comap f q ≤ p
x : M
h : x ∈ comap f (map f p ⊔ q)
y : M
hy : y ∈ (↑p : Set M)
hz : Membership.mem (α := M₂) q ((f : (a : M) → M₂) (x - y) : M₂)
⊢ x ∈ p

Tactic:
simpa using p.add_mem (le hz) hy

Premises used: Submodule.add_mem
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R₂ M₂
hp : IsCoatom p
h : ¬comap f p = ⊤
q : Submodule R M
lt : comap f p < q
rw : p < map f q ⊔ p
⊢ q = ⊤

Tactic:
rw [← comap_map_sup_of_comap_le lt.le, hp.2 (map f q ⊔ p), comap_top]

Premises used: Submodule.comap_map_sup_of_comap_le, LT.lt.le, And.right, Max.max, Submodule.map, Submodule.comap_top
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R₂ M₂
hp : IsCoatom p
h : ¬comap f p = ⊤
q : Submodule R M
lt : comap f p < q
⊢ p < map f q ⊔ p

Tactic:
simpa only [right_lt_sup, map_le_iff_le_comap] using lt.not_ge

Premises used: right_lt_sup, LT.lt.not_ge, Submodule.map_le_iff_le_comap
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p : Submodule R₂ M₂
⊢ Injective (comap f)

Tactic:
have := comap_injective_of_surjective hf
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p : Submodule R₂ M₂
this : Injective (comap f)
rw : (p ≠ ⊤ ∧ ∀ (b : Submodule R M), comap f p < b → b = comap f ⊤) ↔ p ≠ ⊤ ∧ ∀ (b : Submodule R₂ M₂), p < b → b = ⊤
⊢ IsCoatom (comap f p) ↔ IsCoatom p

Tactic:
rw [IsCoatom, IsCoatom, ← comap_top f, this.ne_iff]

Premises used: Function.Injective.ne_iff, IsCoatom, Submodule.comap_top
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p : Submodule R₂ M₂
this : Injective (comap f)
⊢ (p ≠ ⊤ ∧ ∀ (b : Submodule R M), comap f p < b → b = comap f ⊤) ↔ p ≠ ⊤ ∧ ∀ (b : Submodule R₂ M₂), p < b → b = ⊤

Tactic:
and_congr_right fun _ ↦
    ⟨fun h m hm ↦ this (h _ <| comap_strictMono_of_surjective hf hm), fun h m hm ↦ ?_⟩

Premises used: Submodule.comap_strictMono_of_surjective, and_congr_right, Submodule.comap, Iff.intro
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p : Submodule R₂ M₂
this : Injective (comap f)
refine : p ≠ ⊤ → ∀ (h : ∀ (b : Submodule R₂ M₂), p < b → b = ⊤) (m : Submodule R M) (hm : comap f p < m), m = comap f ⊤
⊢ (p ≠ ⊤ ∧ ∀ (b : Submodule R M), comap f p < b → b = comap f ⊤) ↔ p ≠ ⊤ ∧ ∀ (b : Submodule R₂ M₂), p < b → b = ⊤

Tactic:
refine and_congr_right fun _ ↦
    ⟨fun h m hm ↦ this (h _ <| comap_strictMono_of_surjective hf hm), fun h m hm ↦ ?_⟩

Premises used: and_congr_right, Iff.intro
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p : Submodule R₂ M₂
this : Injective (comap f)
h_1 : p ≠ ⊤
h : ∀ (b : Submodule R₂ M₂), p < b → b = ⊤
m : Submodule R M
hm : comap f p < m
rw : m = comap f (map f m)
rw₁ rw₂ : m = m
⊢ m = comap f ⊤

Tactic:
rw [← h _ (lt_map_of_comap_lt_of_surjective hf hm),
    comap_map_eq_self ((comap_mono bot_le).trans hm.le)]

Premises used: Submodule.comap_mono, Submodule.comap_map_eq_self, LT.lt.le, Submodule.lt_map_of_comap_lt_of_surjective, LE.le.trans, bot_le
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p : Submodule R M
le : f.ker ≤ p
hp rwa rwa₁ rwa₂ rwa₃ : IsCoatom p
⊢ IsCoatom (comap f (map f p))

Tactic:
rwa [comap_map_eq_self le]

Premises used: Submodule.comap_map_eq_self
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
ι : Sort u_8
p : ι → Submodule R M
h : f.ker ≤ ⨅ (i : ι), p i
rw : map f (⨅ (i : ι), comap f (map f (p i)))
| ⨅ (i : ι), map f (p i)

Tactic:
rw [← map_comap_eq_of_surjective hf (⨅ _, _), comap_iInf]

Premises used: iInf, Submodule.comap_iInf, Submodule.map_comap_eq_of_surjective
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
ι : Sort u_8
p : ι → Submodule R M
h : f.ker ≤ ⨅ (i : ι), p i
conv_rhs : map f (⨅ (i : ι), p i) = map f (⨅ (i : ι), comap f (map f (p i)))
⊢ map f (⨅ (i : ι), p i) = ⨅ (i : ι), map f (p i)

Tactic:
conv_rhs => rw [← map_comap_eq_of_surjective hf (⨅ _, _), comap_iInf]

Premises used: iInf, Submodule.comap_iInf, Submodule.map_comap_eq_of_surjective
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
ι : Sort u_8
p : ι → Submodule R M
h : f.ker ≤ ⨅ (i : ι), p i
⊢ map f (⨅ (i : ι), p i) = map f (⨅ (i : ι), comap f (map f (p i)))

Tactic:
simp_rw [fun i ↦ comap_map_eq_self (le_iInf_iff.mp h i)]

Premises used: Submodule.comap_map_eq_self, le_iInf_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R₂ M₂
h : p ⋖ q
⊢ comap f p ⋖ comap f q

Tactic:
⟨lt_of_le_of_ne (comap_mono h.1.le) ((comap_injective_of_surjective hf).ne h.1.ne), ?_⟩

Premises used: Submodule.comap_mono, CovBy, Function.Injective.ne, LT.lt.le, Submodule.comap_injective_of_surjective, And.left, And.intro, lt_of_le_of_ne, LT.lt.ne
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R₂ M₂
h : p ⋖ q
refine : ∀ ⦃c : Submodule R M⦄, comap f p < c → ¬c < comap f q
⊢ comap f p ⋖ comap f q

Tactic:
refine ⟨lt_of_le_of_ne (comap_mono h.1.le) ((comap_injective_of_surjective hf).ne h.1.ne), ?_⟩
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R₂ M₂
h : p ⋖ q
N : Submodule R M
h₁ : comap f p < N
h₂ : N < comap f q
⊢ False

Tactic:
h.2 (lt_map_of_comap_lt_of_surjective hf h₁) ?_

Premises used: Submodule.lt_map_of_comap_lt_of_surjective, And.right
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R₂ M₂
h : p ⋖ q
N : Submodule R M
h₁ : comap f p < N
h₂ : N < comap f q
refine : map f N < q
⊢ False

Tactic:
refine h.2 (lt_map_of_comap_lt_of_surjective hf h₁) ?_

Premises used: Submodule.lt_map_of_comap_lt_of_surjective, And.right
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R₂ M₂
h : p ⋖ q
N : Submodule R M
h₁ : comap f p < N
h₂ : N < comap f q
rwa : f.ker ≤ N
⊢ map f N < q

Tactic:
rwa [← comap_lt_comap_iff_of_surjective hf, comap_map_eq, sup_eq_left.mpr]

Premises used: Submodule.comap_lt_comap_iff_of_surjective, Iff.mpr, sup_eq_left, Submodule.comap_map_eq
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R₂ M₂
h : p ⋖ q
N : Submodule R M
h₁ : comap f p < N
h₂ : N < comap f q
⊢ f.ker ≤ N

Tactic:
(LinearMap.ker_le_comap (f : M →ₛₗ[τ₁₂] M₂)).trans h₁.le

Premises used: LT.lt.le, LE.le.trans, LinearMap.ker_le_comap
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R₂ M₂
h : p ⋖ q
N : Submodule R M
h₁ : comap f p < N
h₂ : N < comap f q
⊢ f.ker ≤ N

Tactic:
refine (LinearMap.ker_le_comap (f : M →ₛₗ[τ₁₂] M₂)).trans h₁.le

Premises used: LT.lt.le, LE.le.trans, LinearMap.ker_le_comap
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
⊢ (f.domRestrict S).range = f.range ↔ S ⊔ f.ker = ⊤

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
refine_1 : ∀ (h : (f.domRestrict S).range = f.range), S ⊔ f.ker = ⊤
refine_2 : ∀ (h : S ⊔ f.ker = ⊤), (f.domRestrict S).range = f.range
⊢ (f.domRestrict S).range = f.range ↔ S ⊔ f.ker = ⊤

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : (f.domRestrict S).range = f.range
refine_1 : ⊤ ≤ S ⊔ f.ker
⊢ S ⊔ f.ker = ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : (f.domRestrict S).range = f.range
x : M
refine_1 : Membership.mem (γ := Submodule R M) ⊤ x → x ∈ S ⊔ f.ker
⊢ Membership.mem (γ := Submodule R M) ⊤ x → x ∈ S ⊔ f.ker

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : (f.domRestrict S).range = f.range
x : M
h_1 : Membership.mem (γ := Submodule R M) ⊤ x
⊢ Membership.mem (α := M₂) f.range ((f : (a : M) → M₂) x : M₂)

Tactic:
have : f x ∈ LinearMap.range f := LinearMap.mem_range_self f x
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : (f.domRestrict S).range = f.range
x : M
h_1 : Membership.mem (γ := Submodule R M) ⊤ x
this : Membership.mem (α := M₂) f.range ((f : (a : M) → M₂) x : M₂)
⊢ Membership.mem (α := M₂) (f.domRestrict S).range ((f : (a : M) → M₂) x : M₂)

Tactic:
rw [← h] at this
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : (f.domRestrict S).range = f.range
x : M
h_1 : Membership.mem (γ := Submodule R M) ⊤ x
this : Membership.mem (α := M₂) (f.domRestrict S).range ((f : (a : M) → M₂) x : M₂)
⊢ ∃ (y : ↥S), Eq.{u_5 + 1} (α := M₂) ((f.domRestrict S : (a : ↥S) → M₂) y : M₂) ((f : (a : M) → M₂) x : M₂)

Tactic:
this

Premises used: Set.Mem, setOf, Set.range
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : (f.domRestrict S).range = f.range
x : M
h_1 : Membership.mem (γ := Submodule R M) ⊤ x
this : Membership.mem (α := M₂) (f.domRestrict S).range ((f : (a : M) → M₂) x : M₂)
refine_1 :
  ∀ (y : ↥S) (hy : Eq.{u_5 + 1} (α := M₂) ((f.domRestrict S : (a : ↥S) → M₂) y : M₂) ((f : (a : M) → M₂) x : M₂)),
    x ∈ S ⊔ f.ker
⊢ x ∈ S ⊔ f.ker

Tactic:
obtain ⟨y, hy⟩ : ∃ y : S, f.domRestrict S y = f x := this

Premises used: DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : (f.domRestrict S).range = f.range
x : M
h_1 : Membership.mem (γ := Submodule R M) ⊤ x
y : ↥S
hy : Eq.{u_5 + 1} (α := M₂) ((f.domRestrict S : (a : ↥S) → M₂) y : M₂) ((f : (a : M) → M₂) x : M₂)
⊢ x - (↑y : M) ∈ f.ker

Tactic:
simp [← hy]
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : (f.domRestrict S).range = f.range
x : M
h_1 : Membership.mem (γ := Submodule R M) ⊤ x
y : ↥S
hy : Eq.{u_5 + 1} (α := M₂) ((f.domRestrict S : (a : ↥S) → M₂) y : M₂) ((f : (a : M) → M₂) x : M₂)
⊢ (↑y : M) + (x - (↑y : M)) ∈ S ⊔ f.ker

Tactic:
have : (y : M) + (x - y) ∈ S ⊔ (LinearMap.ker f) := Submodule.add_mem_sup y.2 (by simp [← hy])