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₂
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₂)
this : (↑y : M) + (x - (↑y : M)) ∈ S ⊔ f.ker
⊢ x ∈ S ⊔ f.ker

Tactic:
simpa using 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 : S ⊔ f.ker = ⊤
⊢ (f.domRestrict S).range = f.range

Tactic:
le_antisymm (LinearMap.range_domRestrict_le_range f S) ?_

Premises used: LinearMap.range_domRestrict_le_range, le_antisymm
-- 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 : S ⊔ f.ker = ⊤
refine_2 : f.range ≤ (f.domRestrict S).range
⊢ (f.domRestrict S).range = f.range

Tactic:
refine le_antisymm (LinearMap.range_domRestrict_le_range f S) ?_

Premises used: LinearMap.range_domRestrict_le_range, le_antisymm
-- 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 : S ⊔ f.ker = ⊤
y : M
⊢ y ∈ S ⊔ f.ker

Tactic:
simp [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 : S ⊔ f.ker = ⊤
y : M
refine_2 :
  ∀ (s : M) (hs : s ∈ S) (t : M) (ht : t ∈ f.ker),
    Membership.mem (α := M₂) (f.domRestrict S).range ((f : (a : M) → M₂) (s + t) : M₂)
⊢ Membership.mem (α := M₂) (f.domRestrict S).range ((f : (a : M) → M₂) y : M₂)

Tactic:
obtain ⟨s, hs, t, ht, rfl⟩ : ∃ s, s ∈ S ∧ ∃ t, t ∈ LinearMap.ker f ∧ s + t = y :=
      Submodule.mem_sup.1 (by simp [h])

Premises used: LinearMap.ker, 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₂
S : Submodule R M
h : S ⊔ f.ker = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ f.ker
⊢ Eq.{u_5 + 1} (α := M₂) ((f.domRestrict S : (a : ↥S) → M₂) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) s hs) : M₂)
    ((f : (a : M) → M₂) (s + t) : M₂)

Tactic:
simp [LinearMap.mem_ker.1 ht]

Premises used: LinearMap.mem_ker, 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₂
S : Submodule R M
h : S ⊔ f.ker = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ f.ker
⊢ Membership.mem (α := M₂) (f.domRestrict S).range ((f : (a : M) → M₂) (s + t) : M₂)

Tactic:
exact ⟨⟨s, hs⟩, by simp [LinearMap.mem_ker.1 ht]⟩
-- 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
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
rw : ∀ (hf : f.range = ⊤), (f.domRestrict S).range = ⊤ ↔ S ⊔ f.ker = ⊤
⊢ Surjective.{u_4 + 1, u_5 + 1} (α := ↥S) (β := M₂) (⇑(f.domRestrict S) : (a : ↥S) → M₂) ↔ S ⊔ f.ker = ⊤

Tactic:
rw [← LinearMap.range_eq_top] at hf ⊢

Premises used: LinearMap.range_eq_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₂
S : Submodule R M
hf : f.range = ⊤
rw : (f.domRestrict S).range = f.range ↔ S ⊔ f.ker = ⊤
⊢ (f.domRestrict S).range = ⊤ ↔ S ⊔ f.ker = ⊤

Tactic:
rw [← 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₂
S : Submodule R M
hf : f.range = ⊤
⊢ (f.domRestrict S).range = f.range ↔ S ⊔ f.ker = ⊤

Tactic:
LinearMap.range_domRestrict_eq_range_iff

Premises used: LinearMap.range_domRestrict_eq_range_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
hf : f.range = ⊤
⊢ (f.domRestrict S).range = f.range ↔ S ⊔ f.ker = ⊤

Tactic:
exact LinearMap.range_domRestrict_eq_range_iff

Premises used: LinearMap.range_domRestrict_eq_range_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 τ₁₂
ι : Type u_8
s : Set ι
hs : s.Nonempty
p : ι → Submodule R₂ M₂
hp : Eq.{u_5 + 1} (α := Submodule R₂ M₂) (⨆ i ∈ s, p i) ⊤
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
obtain : ∀ (k : ι) (hk : k ∈ s), Eq.{u_4 + 1} (α := Submodule R M) (⨆ i ∈ s, comap f (p i)) ⊤
⊢ Eq.{u_4 + 1} (α := Submodule R M) (⨆ i ∈ s, comap f (p i)) ⊤

Tactic:
obtain ⟨k, hk⟩ := hs
-- 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 τ₁₂
ι : Type u_8
s : Set ι
p : ι → Submodule R₂ M₂
hp : Eq.{u_5 + 1} (α := Submodule R₂ M₂) (⨆ i ∈ s, p i) ⊤
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
k : ι
hk : k ∈ s
this : (⨆ i ∈ s, comap f (p i)) ⊔ f.ker = ⊤
rw : f.ker ≤ ⨆ i ∈ s, comap f (p i)
⊢ Eq.{u_4 + 1} (α := Submodule R M) (⨆ i ∈ s, comap f (p i)) ⊤

Tactic:
rw [← this, left_eq_sup]

Premises used: left_eq_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 τ₁₂
ι : Type u_8
s : Set ι
p : ι → Submodule R₂ M₂
hp : Eq.{u_5 + 1} (α := Submodule R₂ M₂) (⨆ i ∈ s, p i) ⊤
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
k : ι
hk : k ∈ s
this : (⨆ i ∈ s, comap f (p i)) ⊔ f.ker = ⊤
⊢ f.ker ≤ ⨆ i ∈ s, comap f (p i)

Tactic:
le_trans f.ker_le_comap (le_biSup (fun i ↦ (p i).comap f) hk)

Premises used: Submodule.comap, le_biSup, 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 τ₁₂
ι : Type u_8
s : Set ι
p : ι → Submodule R₂ M₂
hp : Eq.{u_5 + 1} (α := Submodule R₂ M₂) (⨆ i ∈ s, p i) ⊤
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
k : ι
hk : k ∈ s
this : (⨆ i ∈ s, comap f (p i)) ⊔ f.ker = ⊤
⊢ f.ker ≤ ⨆ i ∈ s, comap f (p i)

Tactic:
exact le_trans f.ker_le_comap (le_biSup (fun i ↦ (p i).comap f) hk)

Premises used: Submodule.comap, le_biSup, 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 τ₁₂
ι : Type u_8
s : Set ι
p : ι → Submodule R₂ M₂
hp : Eq.{u_5 + 1} (α := Submodule R₂ M₂) (⨆ i ∈ s, p i) ⊤
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
k : ι
hk : k ∈ s
suffices : (⨆ i ∈ s, comap f (p i)) ⊔ f.ker = ⊤
⊢ Eq.{u_4 + 1} (α := Submodule R M) (⨆ i ∈ s, comap f (p i)) ⊤

Tactic:
suffices (⨆ i ∈ s, (p i).comap f) ⊔ LinearMap.ker f = ⊤ by
    rw [← this, left_eq_sup]; exact le_trans f.ker_le_comap (le_biSup (fun i ↦ (p i).comap f) hk)
-- 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 τ₁₂
ι : Type u_8
s : Set ι
p : ι → Submodule R₂ M₂
hp : Eq.{u_5 + 1} (α := Submodule R₂ M₂) (⨆ i ∈ s, p i) ⊤
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
k : ι
hk : k ∈ s
rw :
  ∀ (hp : Eq.{u_5 + 1} (α := Submodule R₂ M₂) (⨆ (x : Subtype (Membership.mem s)), p (↑x : ι)) ⊤) (f : M →ₛₗ[τ₁₂] M₂)
    (hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)) (k : ι) (hk : k ∈ s),
    (⨆ (x : Subtype (Membership.mem s)), comap f (p (↑x : ι))) ⊔ f.ker = ⊤
⊢ (⨆ i ∈ s, comap f (p i)) ⊔ f.ker = ⊤

Tactic:
rw [iSup_subtype'] at hp ⊢

Premises used: iSup_subtype'
-- 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 τ₁₂
ι : Type u_8
s : Set ι
p : ι → Submodule R₂ M₂
hp : Eq.{u_5 + 1} (α := Submodule R₂ M₂) (⨆ (x : Subtype (Membership.mem s)), p (↑x : ι)) ⊤
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
k : ι
hk : k ∈ s
rw : comap f (map f (⨆ (x : Subtype (Membership.mem s)), comap f (p (↑x : ι)))) = ⊤
rw₁ : comap f (⨆ (x : Subtype (Membership.mem s)), p (↑x : ι)) = ⊤
rw₂ : comap f ⊤ = ⊤
rw₃ rw₄ : Eq.{u_4 + 1} (α := Submodule R M) ⊤ ⊤
⊢ (⨆ (x : Subtype (Membership.mem s)), comap f (p (↑x : ι))) ⊔ f.ker = ⊤

Tactic:
rw [← comap_map_eq, map_iSup_comap_of_surjective hf, hp, comap_top]

Premises used: Submodule.map_iSup_comap_of_surjective, Submodule.comap_top, Submodule.comap_map_eq
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
M : Type u_4
M₂ : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
R : Type u_8
R₂ : Type u_9
inst_2 : Semiring R
inst_3 : Ring R₂
τ₁₂ : R →+* R₂
inst_4 : RingHomSurjective τ₁₂
inst_5 : Module R M
inst_6 : Module R₂ M₂
ι : Type u_10
s : Set ι
hs : s.Nonempty
p : ι → Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.range = ⨆ i ∈ s, p i
this : Eq.{u_5 + 1} (α := Submodule R₂ ↥f.range) (⨆ i ∈ s, comap f.range.subtype (p i)) ⊤
rw :
  Eq.{u_4 + 1} (α := Submodule R M) (⨆ i ∈ s, comap f (p i))
    (⨆ i ∈ s, comap f.rangeRestrict (comap f.range.subtype (p i)))
⊢ Eq.{u_4 + 1} (α := Submodule R M) (⨆ i ∈ s, comap f (p i)) ⊤

Tactic:
rw [← biSup_comap_eq_top_of_surjective s hs _ this _ f.surjective_rangeRestrict]

Premises used: Submodule.biSup_comap_eq_top_of_surjective, LinearMap.surjective_rangeRestrict
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
M : Type u_4
M₂ : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
R : Type u_8
R₂ : Type u_9
inst_2 : Semiring R
inst_3 : Ring R₂
τ₁₂ : R →+* R₂
inst_4 : RingHomSurjective τ₁₂
inst_5 : Module R M
inst_6 : Module R₂ M₂
ι : Type u_10
s : Set ι
hs : s.Nonempty
p : ι → Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.range = ⨆ i ∈ s, p i
this : Eq.{u_5 + 1} (α := Submodule R₂ ↥f.range) (⨆ i ∈ s, comap f.range.subtype (p i)) ⊤
⊢ Eq.{u_4 + 1} (α := Submodule R M) (⨆ i ∈ s, comap f (p i))
    (⨆ i ∈ s, comap f.rangeRestrict (comap f.range.subtype (p i)))

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
M : Type u_4
M₂ : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
R : Type u_8
R₂ : Type u_9
inst_2 : Semiring R
inst_3 : Ring R₂
τ₁₂ : R →+* R₂
inst_4 : RingHomSurjective τ₁₂
inst_5 : Module R M
inst_6 : Module R₂ M₂
ι : Type u_10
s : Set ι
hs : s.Nonempty
p : ι → Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.range = ⨆ i ∈ s, p i
suffices : Eq.{u_5 + 1} (α := Submodule R₂ ↥f.range) (⨆ i ∈ s, comap f.range.subtype (p i)) ⊤
⊢ Eq.{u_4 + 1} (α := Submodule R M) (⨆ i ∈ s, comap f (p i)) ⊤

Tactic:
suffices ⨆ i ∈ s, (p i).comap (LinearMap.range f).subtype = ⊤ by
    rw [← biSup_comap_eq_top_of_surjective s hs _ this _ f.surjective_rangeRestrict]; rfl
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
M : Type u_4
M₂ : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
R : Type u_8
R₂ : Type u_9
inst_2 : Semiring R
inst_3 : Ring R₂
τ₁₂ : R →+* R₂
inst_4 : RingHomSurjective τ₁₂
inst_5 : Module R M
inst_6 : Module R₂ M₂
ι : Type u_10
s : Set ι
hs : s.Nonempty
p : ι → Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.range = ⨆ i ∈ s, p i
⊢ Eq.{u_5 + 1} (α := Submodule R₂ ↥f.range) (⨆ i ∈ s, comap f.range.subtype (p i)) ⊤

Tactic:
hf ▸ biSup_comap_subtype_eq_top s p

Premises used: Submodule.biSup_comap_subtype_eq_top, Eq.rec, Eq.symm
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
M : Type u_4
M₂ : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
R : Type u_8
R₂ : Type u_9
inst_2 : Semiring R
inst_3 : Ring R₂
τ₁₂ : R →+* R₂
inst_4 : RingHomSurjective τ₁₂
inst_5 : Module R M
inst_6 : Module R₂ M₂
ι : Type u_10
s : Set ι
hs : s.Nonempty
p : ι → Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.range = ⨆ i ∈ s, p i
⊢ Eq.{u_5 + 1} (α := Submodule R₂ ↥f.range) (⨆ i ∈ s, comap f.range.subtype (p i)) ⊤

Tactic:
exact hf ▸ biSup_comap_subtype_eq_top s p
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Ring 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'
inl : ∀ (h : p ⊓ f.ker < p' ⊓ f.ker), map f p < map f p' ∨ f.ker ⊓ p < f.ker ⊓ p'
inr : ∀ (h : p ⊔ f.ker < p' ⊔ f.ker), map f p < map f p' ∨ f.ker ⊓ p < f.ker ⊓ p'
⊢ map f p < map f p' ∨ f.ker ⊓ p < f.ker ⊓ p'

Tactic:
obtain (⟨h, -⟩ | ⟨-, h⟩) := Prod.mk_lt_mk.mp <| strictMono_inf_prod_sup (z := LinearMap.ker f) hab

Premises used: Iff.mp, Prod.mk_lt_mk, strictMono_inf_prod_sup
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Ring 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
⊢ map f p < map f p' ∨ f.ker ⊓ p < f.ker ⊓ p'

Tactic:
simpa [inf_comm] using Or.inr h

Premises used: inf_comm, Or.inr
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Ring 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
⊢ map f p < map f p' ∨ f.ker ⊓ p < f.ker ⊓ p'

Tactic:
apply Or.inl <| map_lt_map_of_le_of_sup_lt_sup hab.le h

Premises used: Submodule.map_lt_map_of_le_of_sup_lt_sup, LT.lt.le, Or.inl
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Ring 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'
q : map f p = map f p'
⊢ f.ker ⊓ p < f.ker ⊓ p'

Tactic:
map_strict_mono_or_ker_sup_lt_ker_sup f hab |>.resolve_left q.not_lt

Premises used: Or.resolve_left, Submodule.map_strict_mono_or_ker_sup_lt_ker_sup, Eq.not_lt
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Ring 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'
q : f.ker ⊓ p = f.ker ⊓ p'
⊢ map f p < map f p'

Tactic:
map_strict_mono_or_ker_sup_lt_ker_sup f hab |>.resolve_right q.not_lt

Premises used: Submodule.map_strict_mono_or_ker_sup_lt_ker_sup, Eq.not_lt, Or.resolve_right
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Submodule R M
x : M
rw : Disjoint (R ∙ x) s ↔ ∀ (r : R), r • x ∈ s → r • x = 0
⊢ Disjoint s (R ∙ x) ↔ ∀ (r : R), r • x ∈ s → r • x = 0

Tactic:
rw [disjoint_comm]

Premises used: disjoint_comm
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Submodule R M
x : M
⊢ Disjoint (R ∙ x) s ↔ ∀ (r : R), r • x ∈ s → r • x = 0

Tactic:
simp +contextual [disjoint_def, mem_span_singleton]

Premises used: Submodule.mem_span_singleton, Submodule.disjoint_def
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
K : Type u_3
V : Type u_6
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
x : V
s : Submodule K V
h : x ∉ s
⊢ s < K ∙ x ⊔ s

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
K : Type u_3
V : Type u_6
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Submodule K V
x : V
⊢ Disjoint s (K ∙ x) ↔ x ∈ s → x = 0

Tactic:
simpa +contextual [disjoint_span_singleton'', or_iff_not_imp_left, forall_comm (β := ¬_),
    s.smul_mem_iff] using ⟨fun h ↦ h _ one_ne_zero, fun h _ _ ↦ h⟩

Premises used: forall_comm, Classical.or_iff_not_imp_left, Submodule.smul_mem_iff, Submodule.disjoint_span_singleton''
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
K : Type u_3
V : Type u_6
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Submodule K V
x : V
hx : x ≠ 0
⊢ Disjoint s (K ∙ x) ↔ x ∉ s

Tactic:
simp [disjoint_span_singleton, hx]

Premises used: Submodule.disjoint_span_singleton
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
K : Type u_3
V : Type u_6
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Submodule K V
x : V
hx : x ∉ s
⊢ Disjoint s (K ∙ x)

Tactic:
simp [disjoint_span_singleton, hx]

Premises used: Submodule.disjoint_span_singleton
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
K : Type u_3
V : Type u_6
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Submodule K V
x : V
hs : IsCoatom s
hx : x ∉ s
⊢ IsCompl s (K ∙ x)

Tactic:
⟨disjoint_span_singleton_of_notMem hx, ?_⟩

Premises used: Submodule.disjoint_span_singleton_of_notMem, IsCompl.mk
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
K : Type u_3
V : Type u_6
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Submodule K V
x : V
hs : IsCoatom s
hx : x ∉ s
refine : Codisjoint s (K ∙ x)
⊢ IsCompl s (K ∙ x)

Tactic:
refine ⟨disjoint_span_singleton_of_notMem hx, ?_⟩
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
K : Type u_3
V : Type u_6
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Submodule K V
x : V
hs : IsCoatom s
hx : x ∉ s
⊢ s ⋖ ⊤

Tactic:
rw [← covBy_top_iff] at hs

Premises used: covBy_top_iff
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
K : Type u_3
V : Type u_6
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Submodule K V
x : V
hs : IsCoatom s
hx : x ∉ s
hs₁ : s ⋖ ⊤
⊢ x ∉ s

Tactic:
rw [← covBy_top_iff] at hs

Premises used: covBy_top_iff
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
K : Type u_3
V : Type u_6
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Submodule K V
x : V
hs : s ⋖ ⊤
hx : x ∉ s
⊢ Codisjoint s (K ∙ x)

Tactic:
simpa only [codisjoint_iff, sup_comm, not_lt_top_iff] using hs.2 (covBy_span_singleton_sup hx).1

Premises used: not_lt_top_iff, codisjoint_iff, sup_comm, And.right, And.left, Submodule.covBy_span_singleton_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 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p p' : Submodule R M
rw : p ≤ comap f (map f p') ↔ p ≤ p' ⊔ f.ker
rw₁ rw₂ : p ≤ p' ⊔ f.ker ↔ p ≤ p' ⊔ f.ker
⊢ map f p ≤ map f p' ↔ p ≤ p' ⊔ f.ker

Tactic:
rw [map_le_iff_le_comap, Submodule.comap_map_eq]

Premises used: Submodule.map_le_iff_le_comap, 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 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.ker = ⊥
p p' : Submodule R M
rw : p ≤ p' ⊔ f.ker ↔ p ≤ p'
rw₁ : p ≤ p' ⊔ ⊥ ↔ p ≤ p'
rw₂ rw₃ : p ≤ p' ↔ p ≤ p'
⊢ map f p ≤ map f p' ↔ p ≤ p'

Tactic:
rw [LinearMap.map_le_map_iff, hf, sup_bot_eq]

Premises used: LinearMap.map_le_map_iff, sup_bot_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 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.ker = ⊥
⊢ Injective (map f)

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

Premises used: LinearMap.map_le_map_iff', ge_of_eq, le_antisymm, Iff.mp, Function.Injective, le_of_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 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.range = ⊤
p : Submodule R M
simp_rw : ⊤ ≤ map f p ↔ ⊤ ≤ p ⊔ f.ker
simp_rw₁ : f.range ≤ map f p ↔ ⊤ ≤ p ⊔ f.ker
simp_rw₂ : map f ⊤ ≤ map f p ↔ ⊤ ≤ p ⊔ f.ker
⊢ map f p = ⊤ ↔ p ⊔ f.ker = ⊤

Tactic:
simp_rw [← top_le_iff, ← hf, range_eq_map, LinearMap.map_le_map_iff]

Premises used: LinearMap.map_le_map_iff, top_le_iff, LinearMap.range_eq_map
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := (x : M) → R →ₗ[R] M) (smulRight id) (toSpanSingleton R M)

Tactic:
rfl

Premises used: LinearMap.toSpanSingleton, rfl
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ (toSpanSingleton R M x : (a : R) → M) 1 = x

Tactic:
one_smul _ _

Premises used: one_smul
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x x_1 : M
eq : Eq (α := R →ₗ[R] M) (toSpanSingleton R M x) (toSpanSingleton R M x_1)
⊢ x = x_1

Tactic:
simpa using congr($eq 1)