awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) y : P)
x : M
y : N
hx : Membership.mem (γ := Submodule R M) (span R s) x
hy : Membership.mem (γ := Submodule R N) (span R t) y
mem_mem :
  ∀ (u : M) (v : N) (hu : u ∈ s) (hv : v ∈ t),
    Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) v : P)
zero_left :
  ∀ (v : N) (hv : Membership.mem (γ := Submodule R N) (span R t) v),
    Membership.mem (α := P) P' (((B : (a : M) → N →ₗ[R] P) 0 : (a : N) → P) v : P)
zero_right :
  ∀ (u : M) (hu : Membership.mem (γ := Submodule R M) (span R s) u),
    Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) 0 : P)
add_left :
  ∀ (u₁ u₂ : M) (v : N) (hu₁ : Membership.mem (γ := Submodule R M) (span R s) u₁)
    (hu₂ : Membership.mem (γ := Submodule R M) (span R s) u₂) (hv : Membership.mem (γ := Submodule R N) (span R t) v)
    (huv₁ : Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u₁ : N →ₗ[R] P) : (a : N) → P) v : P))
    (huv₂ : Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u₂ : N →ₗ[R] P) : (a : N) → P) v : P)),
    Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) (u₁ + u₂) : N →ₗ[R] P) : (a : N) → P) v : P)
add_right :
  ∀ (u : M) (v₁ v₂ : N) (hu : Membership.mem (γ := Submodule R M) (span R s) u)
    (hv₁ : Membership.mem (γ := Submodule R N) (span R t) v₁) (hv₂ : Membership.mem (γ := Submodule R N) (span R t) v₂)
    (huv₁ : Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) v₁ : P))
    (huv₂ : Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) v₂ : P)),
    Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) (v₁ + v₂) : P)
⊢ Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) y : P)
have smul_left : ∀ (t_1 : R) (u : M) (v : N) (hu : Membership.mem (γ := Submodule R M) (span R s) u)
  (hv : Membership.mem (γ := Submodule R N) (span R t) v)
  (huv : Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) v : P)),
  Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) (t_1 • u) : N →ₗ[R] P) : (a : N) → P) v : P)
Tactic: induction hx, hy using span_induction₂ with
  | mem_mem u v hu hv => exact hB u hu v hv
  | zero_left v hv => simp
  | zero_right u hu => simp
  | add_left u₁ u₂ v hu₁ hu₂ hv huv₁ huv₂ => simpa using add_mem huv₁ huv₂
  | add_right u v₁ v₂ hu hv₁ hv₂ huv₁ huv₂ => simpa using add_mem huv₁ huv₂
  | smul_left t u v hu hv huv => simpa using Submodule.smul_mem _ _ huv
  | smul_right t u v hu hv huv => simpa using Submodule.smul_mem _ _ huv
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
⊢ Eq.{u_4 + 1} (α := Submodule R ↥(⨆ i ∈ s, p i)) (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i)) ⊤
have refine : ∀ (x : ↥(⨆ i ∈ s, p i)) (x : M) (hx : Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x),
  Membership.mem (γ := Submodule R ↥(⨆ i ∈ s, p i)) ⊤
      (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x) x hx) →
    Membership.mem (γ := Submodule R ↥(⨆ i ∈ s, p i)) (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i))
      (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x) x hx)
Tactic: refine eq_top_iff.mpr fun ⟨x, hx⟩ _ ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x_1 : ↥(⨆ i ∈ s, p i)
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x
h :
  Membership.mem (γ := Submodule R ↥(⨆ i ∈ s, p i)) ⊤
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x) x hx)
this :
  Membership.mem (γ := Submodule R M)
    (map (M := ↥(⨆ i ∈ s, p i)) (Submodule.subtype (⨆ i ∈ s, p i))
      (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i)))
    x
⊢ Membership.mem (γ := Submodule R ↥(⨆ i ∈ s, p i)) (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i))
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x) x hx)
have obtain : ∀ (y : ↥(⨆ i ∈ s, p i))
  (hy : Membership.mem (γ := Submodule R ↥(⨆ i ∈ s, p i)) (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i)) y)
  (hx :
    Membership.mem (α := M) (γ := Submodule R M) (⨆ i ∈ s, p i)
      ((Submodule.subtype (⨆ i ∈ s, p i) : (a : ↥(⨆ i ∈ s, p i)) → M) y : M)),
  Membership.mem (α := ↥(⨆ i ∈ s, p i)) (γ := Submodule R ↥(⨆ i ∈ s, p i)) ⊤
      (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x)
          ((Submodule.subtype (⨆ i ∈ s, p i) : (a : ↥(⨆ i ∈ s, p i)) → M) y) hx :
        ↥(⨆ i ∈ s, p i)) →
    ∀
      (this :
        Membership.mem (α := M) (γ := Submodule R M)
          (map (M := ↥(⨆ i ∈ s, p i)) (Submodule.subtype (⨆ i ∈ s, p i))
            (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i)))
          ((Submodule.subtype (⨆ i ∈ s, p i) : (a : ↥(⨆ i ∈ s, p i)) → M) y : M)),
      Membership.mem (α := ↥(⨆ i ∈ s, p i)) (γ := Submodule R ↥(⨆ i ∈ s, p i))
        (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i))
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x)
            ((Submodule.subtype (⨆ i ∈ s, p i) : (a : ↥(⨆ i ∈ s, p i)) → M) y) hx :
          ↥(⨆ i ∈ s, p i))
Tactic: obtain ⟨y, hy, rfl⟩ := Submodule.mem_map.mp this
Cleared hypotheses: x, hx, h, this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x_1 : ↥(⨆ i ∈ s, p i)
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x
h :
  Membership.mem (γ := Submodule R ↥(⨆ i ∈ s, p i)) ⊤
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x) x hx)
⊢ Membership.mem (γ := Submodule R ↥(⨆ i ∈ s, p i)) (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i))
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x) x hx)
have suffices : Membership.mem (γ := Submodule R M)
  (map (M := ↥(⨆ i ∈ s, p i)) (Submodule.subtype (⨆ i ∈ s, p i))
    (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i)))
  x
Tactic: suffices x ∈ (⨆ i ∈ s, (p i).comap (⨆ i ∈ s, p i).subtype).map (⨆ i ∈ s, (p i)).subtype by
    obtain ⟨y, hy, rfl⟩ := Submodule.mem_map.mp this
    exact hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x_1 : ↥(⨆ i ∈ s, p i)
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x
h :
  Membership.mem (γ := Submodule R ↥(⨆ i ∈ s, p i)) ⊤
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x) x hx)
⊢ Membership.mem (γ := Submodule R M)
    (map (M := ↥(⨆ i ∈ s, p i)) (Submodule.subtype (⨆ i ∈ s, p i))
      (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i)))
    x
have suffices : ∀ i ∈ s,
  map (M := ↥(⨆ i ∈ s, p i)) (Submodule.subtype (⨆ i ∈ s, p i)) (comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i)) = p i
Tactic: suffices ∀ i ∈ s, (comap (⨆ i ∈ s, p i).subtype (p i)).map (⨆ i ∈ s, p i).subtype = p i by
    simpa only [map_iSup, biSup_congr this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x_1 : ↥(⨆ i ∈ s, p i)
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x
h :
  Membership.mem (γ := Submodule R ↥(⨆ i ∈ s, p i)) ⊤
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x) x hx)
i : ι
hi : i ∈ s
⊢ map (M := ↥(⨆ i ∈ s, p i)) (Submodule.subtype (⨆ i ∈ s, p i)) (comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i)) = p i
have rw : p i ≤ ⨆ i ∈ s, p i
Tactic: rw [map_comap_eq, range_subtype, inf_eq_right]
-- 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 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
N : Submodule R M
f : LinearMap.{u_1, u_2, u_4, u_5} σ₁₂ (↥N) M₂
h : f ≠ 0
s : Set (Submodule R M)
hs : sSup s = N
⊢ sSup (comap N.subtype '' s) = ⊤
have hs₁ : ⨆ a ∈ s, a = N
Tactic: rw [sSup_eq_iSup] at 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 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
N : Submodule R M
f : LinearMap.{u_1, u_2, u_4, u_5} σ₁₂ (↥N) M₂
h : f ≠ 0
s : Set (Submodule R M)
hs : ⨆ a ∈ s, a = N
⊢ sSup (comap N.subtype '' s) = ⊤
have rw : Eq.{u_4 + 1} (α := Submodule R ↥N) (⨆ a ∈ s, comap N.subtype a) ⊤
Tactic: rw [sSup_image, ← hs, biSup_comap_subtype_eq_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 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
N : Submodule R M
f : LinearMap.{u_1, u_2, u_4, u_5} σ₁₂ (↥N) M₂
h : f ≠ 0
s : Set (Submodule R M)
hs : ⨆ a ∈ s, a = N
rw : Eq.{u_4 + 1} (α := Submodule R ↥N) (⨆ a ∈ s, comap N.subtype a) ⊤
⊢ sSup (comap N.subtype '' s) = ⊤
have rw₁ : Eq.{u_4 + 1} (α := Submodule R ↥(⨆ a ∈ s, a)) (⨆ a ∈ s, comap (Submodule.subtype (⨆ a ∈ s, a)) a) ⊤
Tactic: rw [sSup_image, ← hs, biSup_comap_subtype_eq_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 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
N : Submodule R M
f : LinearMap.{u_1, u_2, u_4, u_5} σ₁₂ (↥N) M₂
h : f ≠ 0
s : Set (Submodule R M)
hs : ⨆ a ∈ s, a = N
rw : Eq.{u_4 + 1} (α := Submodule R ↥N) (⨆ a ∈ s, comap N.subtype a) ⊤
rw₁ : Eq.{u_4 + 1} (α := Submodule R ↥(⨆ a ∈ s, a)) (⨆ a ∈ s, comap (Submodule.subtype (⨆ a ∈ s, a)) a) ⊤
⊢ sSup (comap N.subtype '' s) = ⊤
have rw₂ : Eq.{u_4 + 1} (α := Submodule R ↥(⨆ a ∈ s, a)) ⊤ ⊤
Tactic: rw [sSup_image, ← hs, biSup_comap_subtype_eq_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 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
inst_6 : RingHomSurjective σ₁₂
p q : Submodule R₂ M₂
hp : p ≤ f.range
⊢ comap f p ≤ comap f q ↔ p ≤ q
have rw : map f (comap f p) ≤ q ↔ p ≤ q
Tactic: rw [← Submodule.map_le_iff_le_comap, Submodule.map_comap_eq_of_le hp]
-- 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 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
inst_6 : RingHomSurjective σ₁₂
p q : Submodule R₂ M₂
hp : p ≤ f.range
rw : map f (comap f p) ≤ q ↔ p ≤ q
⊢ comap f p ≤ comap f q ↔ p ≤ q
have rw₁ : p ≤ q ↔ p ≤ q
Tactic: rw [← Submodule.map_le_iff_le_comap, Submodule.map_comap_eq_of_le hp]
-- 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 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
inst_6 : RingHomSurjective σ₁₂
p q : Submodule R₂ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
hp : p ≤ f.range
hq : q ≤ f.range
⊢ comap f (p ⊔ q) = comap f p ⊔ comap f q
have a : map f (comap f (p ⊔ q)) = map f (comap f p ⊔ comap f q)
Tactic: apply map_injective_of_injective 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 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
inst_6 : RingHomSurjective σ₁₂
p q : Submodule R₂ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
hp : p ≤ f.range
hq : q ≤ f.range
⊢ map f (comap f (p ⊔ q)) = map f (comap f p ⊔ comap f q)
have a : p ⊔ q ≤ f.range
Tactic: rw [map_sup, map_comap_eq_self, map_comap_eq_self hp, map_comap_eq_self hq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
⊢ (s ⊔ t) ⊓ p = s ⊔ t ⊓ p
have h : ∀ (x : M), x ∈ (s ⊔ t) ⊓ p ↔ x ∈ s ⊔ t ⊓ p
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x : M
⊢ x ∈ (s ⊔ t) ⊓ p ↔ x ∈ s ⊔ t ⊓ p
have h : (∃ y ∈ s, ∃ z ∈ t, y + z = x) ∧ x ∈ p ↔ ∃ y ∈ s, ∃ (z : M), (z ∈ t ∧ z ∈ p) ∧ y + z = x
Tactic: simp only [mem_sup, mem_inf]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x : M
⊢ (∃ y ∈ s, ∃ z ∈ t, y + z = x) ∧ x ∈ p ↔ ∃ y ∈ s, ∃ (z : M), (z ∈ t ∧ z ∈ p) ∧ y + z = x
have h : (∃ y ∈ s, ∃ z ∈ t, y + z = x) ∧ x ∈ p → ∃ y ∈ s, ∃ (z : M), (z ∈ t ∧ z ∈ p) ∧ y + z = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x : M
h : (∃ y ∈ s, ∃ z ∈ t, y + z = x) ∧ x ∈ p → ∃ y ∈ s, ∃ (z : M), (z ∈ t ∧ z ∈ p) ∧ y + z = x
⊢ (∃ y ∈ s, ∃ z ∈ t, y + z = x) ∧ x ∈ p ↔ ∃ y ∈ s, ∃ (z : M), (z ∈ t ∧ z ∈ p) ∧ y + z = x
have h₁ : (∃ y ∈ s, ∃ (z : M), (z ∈ t ∧ z ∈ p) ∧ y + z = x) → (∃ y ∈ s, ∃ z ∈ t, y + z = x) ∧ x ∈ p
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x : M
hx : x ∈ p
y : M
hy : y ∈ s
z : M
hz : z ∈ t
hyzx : y + z = x
⊢ ∃ y ∈ s, ∃ (z : M), (z ∈ t ∧ z ∈ p) ∧ y + z = x
have h : z ∈ p
Tactic: refine ⟨y, hy, z, ⟨hz, ?_⟩, hyzx⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (hypothesis)
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x : M
hx : x ∈ p
y : M
hy : y ∈ s
z : M
hz : z ∈ t
hyzx : y + z = x
⊢ z ∈ p
have hyzx₁ : z = -y + x
Tactic: rw [← add_right_inj, neg_add_cancel_left] at hyzx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x y : M
hy : y ∈ s
z : M
hyzx : y + z = x
hz : z ∈ t
hz' : z ∈ p
⊢ (∃ y ∈ s, ∃ z ∈ t, y + z = x) ∧ x ∈ p
have h : x ∈ p
Tactic: refine ⟨⟨y, hy, z, hz, hyzx⟩, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t p : Submodule R M
hps : p ≤ s
hnps : -p ≤ s
⊢ s ⊓ t ⊔ p = s ⊓ (t ⊔ p)
have rw : p ⊔ s ⊓ t = s ⊓ (t ⊔ p)
Tactic: rw [sup_comm, inf_comm, ← sup_inf_assoc_of_le_of_neg_le t hps hnps, inf_comm, sup_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t p : Submodule R M
hps : p ≤ s
hnps : -p ≤ s
rw : p ⊔ s ⊓ t = s ⊓ (t ⊔ p)
⊢ s ⊓ t ⊔ p = s ⊓ (t ⊔ p)
have rw₁ : p ⊔ t ⊓ s = s ⊓ (t ⊔ p)
Tactic: rw [sup_comm, inf_comm, ← sup_inf_assoc_of_le_of_neg_le t hps hnps, inf_comm, sup_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t p : Submodule R M
hps : p ≤ s
hnps : -p ≤ s
rw : p ⊔ s ⊓ t = s ⊓ (t ⊔ p)
rw₁ : p ⊔ t ⊓ s = s ⊓ (t ⊔ p)
⊢ s ⊓ t ⊔ p = s ⊓ (t ⊔ p)
have rw₂ : (p ⊔ t) ⊓ s = s ⊓ (t ⊔ p)
Tactic: rw [sup_comm, inf_comm, ← sup_inf_assoc_of_le_of_neg_le t hps hnps, inf_comm, sup_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t p : Submodule R M
hps : p ≤ s
hnps : -p ≤ s
rw : p ⊔ s ⊓ t = s ⊓ (t ⊔ p)
rw₁ : p ⊔ t ⊓ s = s ⊓ (t ⊔ p)
rw₂ : (p ⊔ t) ⊓ s = s ⊓ (t ⊔ p)
⊢ s ⊓ t ⊔ p = s ⊓ (t ⊔ p)
have rw₃ : s ⊓ (p ⊔ t) = s ⊓ (t ⊔ p)
Tactic: rw [sup_comm, inf_comm, ← sup_inf_assoc_of_le_of_neg_le t hps hnps, inf_comm, sup_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t p : Submodule R M
hps : p ≤ s
hnps : -p ≤ s
rw : p ⊔ s ⊓ t = s ⊓ (t ⊔ p)
rw₁ : p ⊔ t ⊓ s = s ⊓ (t ⊔ p)
rw₂ : (p ⊔ t) ⊓ s = s ⊓ (t ⊔ p)
rw₃ : s ⊓ (p ⊔ t) = s ⊓ (t ⊔ p)
⊢ s ⊓ t ⊔ p = s ⊓ (t ⊔ p)
have rw₄ : s ⊓ (t ⊔ p) = s ⊓ (t ⊔ p)
Tactic: rw [sup_comm, inf_comm, ← sup_inf_assoc_of_le_of_neg_le t hps hnps, inf_comm, sup_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
⊢ Eq (α := Submodule R M) (span R (-s)) (-span R s)
have a : LE.le (α := Submodule R M) (span R (-s)) (-span R s)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
a : LE.le (α := Submodule R M) (span R (-s)) (-span R s)
⊢ Eq (α := Submodule R M) (span R (-s)) (-span R s)
have a₁ : LE.le (α := Submodule R M) (-span R s) (span R (-s))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
⊢ LE.le (α := Submodule R M) (span R (-s)) (-span R s)
have a : s ⊆ (↑(span R s) : Set M)
Tactic: rw [span_le, coe_set_neg, ← Set.neg_subset, neg_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
⊢ LE.le (α := Submodule R M) (-span R s) (span R (-s))
have a : -s ⊆ (↑(span R (-s)) : Set M)
Tactic: rw [neg_le, span_le, coe_set_neg, ← Set.neg_subset]
-- 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
⊢ comap f (map f p) = p ⊔ f.ker
have refine : comap f (map f p) ≤ p ⊔ f.ker
Tactic: refine le_antisymm ?_ (sup_le (le_comap_map _ _) (comap_mono bot_le))
-- 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 τ₁₂
p p' : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
hab : p ≤ p'
h : p ⊔ f.ker < p' ⊔ f.ker
⊢ map f p < map f p'
have h₁ : comap f (map f p) < comap f (map f p')
Tactic: simp_rw [← comap_map_eq] at h
Cleared hypotheses: 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₂
p : Submodule R M
h : f.ker ≤ p
⊢ comap f (map f p) = p
have rw : p ⊔ f.ker = p
Tactic: rw [Submodule.comap_map_eq, sup_of_le_left 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₂
p : Submodule R M
h : f.ker ≤ p
rw : p ⊔ f.ker = p
⊢ comap f (map f p) = p
have rw₁ : p = p
Tactic: rw [Submodule.comap_map_eq, sup_of_le_left 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₂
p : Submodule R M
q : Submodule R₂ M₂
le : comap f q ≤ p
⊢ comap f (map f p ⊔ q) = p
have refine : ∀ (x : M) (h : x ∈ comap f (map f p ⊔ q)), x ∈ p
Tactic: refine le_antisymm (fun x h ↦ ?_) (map_le_iff_le_comap.mp le_sup_left)
-- 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
q : Submodule R₂ M₂
le : comap f q ≤ p
x : M
h : x ∈ comap f (map f p ⊔ q)
⊢ x ∈ p
have 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
Tactic: obtain ⟨_, ⟨y, hy, rfl⟩, z, hz, eq⟩ := mem_sup.mp h
-- 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₂
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
⊢ x ∈ p
have eq₁ : z = (f : (a : M) → M₂) (x - y)
Tactic: rw [add_comm, ← eq_sub_iff_add_eq, ← map_sub] at eq
Cleared hypotheses: eq
-- 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₂
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)
⊢ x ∈ p
have hz₁ : Membership.mem (α := M₂) q ((f : (a : M) → M₂) (x - y) : M₂)
Tactic: subst eq
Cleared hypotheses: z, hz, eq