awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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
⊢ q = ⊤
have rw : p < map f q ⊔ p
Tactic: rw [← comap_map_sup_of_comap_le lt.le, hp.2 (map f q ⊔ p), comap_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (hypothesis)
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₂
⊢ IsCoatom (comap f p) ↔ IsCoatom p
have this : Injective (comap f)
Tactic: have := comap_injective_of_surjective hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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)
⊢ IsCoatom (comap f p) ↔ IsCoatom p
have rw : (p ≠ ⊤ ∧ ∀ (b : Submodule R M), comap f p < b → b = comap f ⊤) ↔ p ≠ ⊤ ∧ ∀ (b : Submodule R₂ M₂), p < b → b = ⊤
Tactic: rw [IsCoatom, IsCoatom, ← comap_top f, this.ne_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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 = ⊤
have refine : p ≠ ⊤ → ∀ (h : ∀ (b : Submodule R₂ M₂), p < b → b = ⊤) (m : Submodule R M) (hm : comap f p < m), m = comap f ⊤
Tactic: refine and_congr_right fun _ ↦
    ⟨fun h m hm ↦ this (h _ <| comap_strictMono_of_surjective hf hm), fun h m hm ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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
⊢ m = comap f ⊤
have rw : m = comap f (map f m)
Tactic: rw [← h _ (lt_map_of_comap_lt_of_surjective hf hm),
    comap_map_eq_self ((comap_mono bot_le).trans hm.le)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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)
⊢ m = comap f ⊤
have rw₁ : m = m
Tactic: rw [← h _ (lt_map_of_comap_lt_of_surjective hf hm),
    comap_map_eq_self ((comap_mono bot_le).trans hm.le)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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
| ⨅ (i : ι), map f (p i)
have rw : map f (⨅ (i : ι), comap f (map f (p i)))
Tactic: rw [← map_comap_eq_of_surjective hf (⨅ _, _), comap_iInf]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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) = ⨅ (i : ι), map f (p i)
have conv_rhs : map f (⨅ (i : ι), p i) = map f (⨅ (i : ι), comap f (map f (p i)))
Tactic: conv_rhs => rw [← map_comap_eq_of_surjective hf (⨅ _, _), comap_iInf]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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
have refine : ∀ ⦃c : Submodule R M⦄, comap f p < c → ¬c < comap f q
Tactic: refine ⟨lt_of_le_of_ne (comap_mono h.1.le) ((comap_injective_of_surjective hf).ne h.1.ne), ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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
have refine : map f N < q
Tactic: refine h.2 (lt_map_of_comap_lt_of_surjective hf h₁) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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
⊢ map f N < q
have rwa : f.ker ≤ N
Tactic: rwa [← comap_lt_comap_iff_of_surjective hf, comap_map_eq, sup_eq_left.mpr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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 = ⊤
have refine_1 : ∀ (h : (f.domRestrict S).range = f.range), S ⊔ f.ker = ⊤
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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 = ⊤
⊢ (f.domRestrict S).range = f.range ↔ S ⊔ f.ker = ⊤
have refine_2 : ∀ (h : S ⊔ f.ker = ⊤), (f.domRestrict S).range = f.range
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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
⊢ S ⊔ f.ker = ⊤
have refine_1 : ⊤ ≤ S ⊔ f.ker
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (hypothesis)
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
⊢ x ∈ S ⊔ f.ker
have this : Membership.mem (α := M₂) f.range ((f : (a : M) → M₂) x : M₂)
Tactic: have : f x ∈ LinearMap.range f := LinearMap.mem_range_self f x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (hypothesis)
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₂)
⊢ x ∈ S ⊔ f.ker
have this₁ : Membership.mem (α := M₂) (f.domRestrict S).range ((f : (a : M) → M₂) x : M₂)
Tactic: rw [← h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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₂)
⊢ x ∈ S ⊔ f.ker
have 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
Tactic: obtain ⟨y, hy⟩ : ∃ y : S, f.domRestrict S y = f x := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (hypothesis)
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 ∈ S ⊔ f.ker
have this : (↑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])
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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
have refine_2 : f.range ≤ (f.domRestrict S).range
Tactic: refine le_antisymm (LinearMap.range_domRestrict_le_range f S) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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
⊢ Membership.mem (α := M₂) (f.domRestrict S).range ((f : (a : M) → M₂) y : M₂)
have 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₂)
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])
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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₂)
⊢ Surjective.{u_4 + 1, u_5 + 1} (α := ↥S) (β := M₂) (⇑(f.domRestrict S) : (a : ↥S) → M₂) ↔ S ⊔ f.ker = ⊤
have rw : ∀ (hf : f.range = ⊤), (f.domRestrict S).range = ⊤ ↔ S ⊔ f.ker = ⊤
Tactic: rw [← LinearMap.range_eq_top] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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 = ⊤ ↔ S ⊔ f.ker = ⊤
have rw : (f.domRestrict S).range = f.range ↔ S ⊔ f.ker = ⊤
Tactic: rw [← hf]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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₂)
⊢ Eq.{u_4 + 1} (α := Submodule R M) (⨆ i ∈ s, comap f (p i)) ⊤
have obtain : ∀ (k : ι) (hk : k ∈ s), Eq.{u_4 + 1} (α := Submodule R M) (⨆ i ∈ s, comap f (p i)) ⊤
Tactic: obtain ⟨k, hk⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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 = ⊤
⊢ Eq.{u_4 + 1} (α := Submodule R M) (⨆ i ∈ s, comap f (p i)) ⊤
have rw : f.ker ≤ ⨆ i ∈ s, comap f (p i)
Tactic: rw [← this, left_eq_sup]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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
⊢ Eq.{u_4 + 1} (α := Submodule R M) (⨆ i ∈ s, comap f (p i)) ⊤
have suffices : (⨆ i ∈ s, comap f (p i)) ⊔ f.ker = ⊤
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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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
⊢ (⨆ i ∈ s, comap f (p i)) ⊔ f.ker = ⊤
have 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 = ⊤
Tactic: rw [iSup_subtype'] at hp ⊢
Cleared hypotheses: hp, f, hf, k, hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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
⊢ (⨆ (x : Subtype (Membership.mem s)), comap f (p (↑x : ι))) ⊔ f.ker = ⊤
have rw : comap f (map f (⨆ (x : Subtype (Membership.mem s)), comap f (p (↑x : ι)))) = ⊤
Tactic: rw [← comap_map_eq, map_iSup_comap_of_surjective hf, hp, comap_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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 : ι)))) = ⊤
⊢ (⨆ (x : Subtype (Membership.mem s)), comap f (p (↑x : ι))) ⊔ f.ker = ⊤
have rw₁ : comap f (⨆ (x : Subtype (Membership.mem s)), p (↑x : ι)) = ⊤
Tactic: rw [← comap_map_eq, map_iSup_comap_of_surjective hf, hp, comap_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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 : ι)) = ⊤
⊢ (⨆ (x : Subtype (Membership.mem s)), comap f (p (↑x : ι))) ⊔ f.ker = ⊤
have rw₂ : comap f ⊤ = ⊤
Tactic: rw [← comap_map_eq, map_iSup_comap_of_surjective hf, hp, comap_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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 ⊤ = ⊤
⊢ (⨆ (x : Subtype (Membership.mem s)), comap f (p (↑x : ι))) ⊔ f.ker = ⊤
have rw₃ : Eq.{u_4 + 1} (α := Submodule R M) ⊤ ⊤
Tactic: rw [← comap_map_eq, map_iSup_comap_of_surjective hf, hp, comap_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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)) ⊤
have 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)))
Tactic: rw [← biSup_comap_eq_top_of_surjective s hs _ this _ f.surjective_rangeRestrict]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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_4 + 1} (α := Submodule R M) (⨆ i ∈ s, comap f (p i)) ⊤
have suffices : Eq.{u_5 + 1} (α := Submodule R₂ ↥f.range) (⨆ i ∈ s, comap f.range.subtype (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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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'
⊢ map f p < map f p' ∨ f.ker ⊓ p < f.ker ⊓ p'
have inl : ∀ (h : p ⊓ f.ker < p' ⊓ f.ker), 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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'
⊢ map f p < map f p' ∨ f.ker ⊓ p < f.ker ⊓ p'
have inr : ∀ (h : p ⊔ f.ker < p' ⊔ f.ker), 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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 s (R ∙ x) ↔ ∀ (r : R), r • x ∈ s → r • x = 0
have rw : Disjoint (R ∙ x) s ↔ ∀ (r : R), r • x ∈ s → r • x = 0
Tactic: rw [disjoint_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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)
have refine : Codisjoint s (K ∙ x)
Tactic: refine ⟨disjoint_span_singleton_of_notMem hx, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (hypothesis)
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
⊢ Codisjoint s (K ∙ x)
have hs₁ : s ⋖ ⊤
Tactic: rw [← covBy_top_iff] at hs
Cleared hypotheses: hs, hx