awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
Goal:
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
f : M →ₗ[R] N →ₗ[R] P
s : Submodule R M
t : ι → Submodule R N
simp_rw :
  map₂ f (span R (↑s : Set M)) (⨆ (i : ι), span R (↑(t i) : Set N)) =
    ⨆ (i : ι),
      span R
        (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) (↑s : Set M)
          (↑(t i) : Set N))
simp_rw₁ :
  map₂ f (span R (↑s : Set M)) (span R (⋃ (i : ι), (↑(t i) : Set N))) =
    span R
      (⋃ (i : ι),
        image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) (↑s : Set M)
          (↑(t i) : Set N))
⊢ map₂ f (span R (↑s : Set M)) (⨆ (i : ι), span R (↑(t i) : Set N)) =
    ⨆ (i : ι), map₂ f (span R (↑s : Set M)) (span R (↑(t i) : Set N))
have simp_rw₂ : Eq.{u_4 + 1} (α := Submodule R P)
  (span R
    (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) (↑s : Set M)
      (⋃ (i : ι), (↑(t i) : Set N))))
  (span R
    (⋃ (i : ι),
      image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) (↑s : Set M)
        (↑(t i) : Set N)))
Tactic: simp_rw [map₂_span_span, ← span_iUnion, map₂_span_span, Set.image2_iUnion_right]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
f : M →ₗ[R] N →ₗ[R] P
m : M
⊢ map₂ f (R ∙ m) = map (σ₁₂ := RingHom.id R) ((f : (a : M) → N →ₗ[R] P) m)
have h : ∀ (s : Submodule R N), map₂ f (R ∙ m) s = map (σ₁₂ := RingHom.id R) ((f : (a : M) → N →ₗ[R] P) m) s
Tactic: funext s
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
f : M →ₗ[R] N →ₗ[R] P
m : M
s : Submodule R N
⊢ map₂ f (R ∙ m) s = map (σ₁₂ := RingHom.id R) ((f : (a : M) → N →ₗ[R] P) m) s
have h : map₂ f (R ∙ m) (span R (↑s : Set N)) = map (σ₁₂ := RingHom.id R) ((f : (a : M) → N →ₗ[R] P) m) (span R (↑s : Set N))
Tactic: rw [← span_eq s, map₂_span_span, image2_singleton_left, map_span]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
f : M →ₗ[R] N →ₗ[R] P
m : M
s : Submodule R N
h : map₂ f (R ∙ m) (span R (↑s : Set N)) = map (σ₁₂ := RingHom.id R) ((f : (a : M) → N →ₗ[R] P) m) (span R (↑s : Set N))
⊢ map₂ f (R ∙ m) s = map (σ₁₂ := RingHom.id R) ((f : (a : M) → N →ₗ[R] P) m) s
have h₁ : Eq.{u_4 + 1} (α := Submodule R P)
  (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) {m} (↑s : Set N)))
  (map (σ₁₂ := RingHom.id R) ((f : (a : M) → N →ₗ[R] P) m) (span R (↑s : Set N)))
Tactic: rw [← span_eq s, map₂_span_span, image2_singleton_left, map_span]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
f : M →ₗ[R] N →ₗ[R] P
m : M
s : Submodule R N
h : map₂ f (R ∙ m) (span R (↑s : Set N)) = map (σ₁₂ := RingHom.id R) ((f : (a : M) → N →ₗ[R] P) m) (span R (↑s : Set N))
h₁ :
  Eq.{u_4 + 1} (α := Submodule R P)
    (span R
      (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) {m} (↑s : Set N)))
    (map (σ₁₂ := RingHom.id R) ((f : (a : M) → N →ₗ[R] P) m) (span R (↑s : Set N)))
⊢ map₂ f (R ∙ m) s = map (σ₁₂ := RingHom.id R) ((f : (a : M) → N →ₗ[R] P) m) s
have h₂ : Eq.{u_4 + 1} (α := Submodule R P)
  (span R ((fun (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) '' (↑s : Set N)))
  (map (σ₁₂ := RingHom.id R) ((f : (a : M) → N →ₗ[R] P) m) (span R (↑s : Set N)))
Tactic: rw [← span_eq s, map₂_span_span, image2_singleton_left, map_span]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
f : M →ₗ[R] N →ₗ[R] P
m : M
s : Submodule R N
h : map₂ f (R ∙ m) (span R (↑s : Set N)) = map (σ₁₂ := RingHom.id R) ((f : (a : M) → N →ₗ[R] P) m) (span R (↑s : Set N))
h₁ :
  Eq.{u_4 + 1} (α := Submodule R P)
    (span R
      (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) {m} (↑s : Set N)))
    (map (σ₁₂ := RingHom.id R) ((f : (a : M) → N →ₗ[R] P) m) (span R (↑s : Set N)))
h₂ :
  Eq.{u_4 + 1} (α := Submodule R P)
    (span R ((fun (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) '' (↑s : Set N)))
    (map (σ₁₂ := RingHom.id R) ((f : (a : M) → N →ₗ[R] P) m) (span R (↑s : Set N)))
⊢ map₂ f (R ∙ m) s = map (σ₁₂ := RingHom.id R) ((f : (a : M) → N →ₗ[R] P) m) s
have h₃ : Eq.{u_4 + 1} (α := Submodule R P)
  (span R ((fun (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) '' (↑s : Set N)))
  (span R ((⇑((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) '' (↑s : Set N)))
Tactic: rw [← span_eq s, map₂_span_span, image2_singleton_left, map_span]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
f : M →ₗ[R] N →ₗ[R] P
s : Submodule R M
n : N
⊢ map₂ f s (R ∙ n) = map (σ₁₂ := RingHom.id R) ((f.flip : (a : N) → M →ₗ[R] P) n) s
have rw : map₂ f s (R ∙ n) = map₂ f.flip (R ∙ n) s
Tactic: rw [← map₂_span_singleton_eq_map, map₂_flip]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
f : M →ₗ[R] N →ₗ[R] P
s : Submodule R M
n : N
rw : map₂ f s (R ∙ n) = map₂ f.flip (R ∙ n) s
⊢ map₂ f s (R ∙ n) = map (σ₁₂ := RingHom.id R) ((f.flip : (a : N) → M →ₗ[R] P) n) s
have rw₁ : map₂ f s (R ∙ n) = map₂ f s (R ∙ n)
Tactic: rw [← map₂_span_singleton_eq_map, map₂_flip]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
M₂ : Type u_5
inst_7 : AddCommMonoid M₂
inst_8 : Module R M₂
f : M₂ →ₗ[R] N →ₗ[R] P
g : M →ₗ[R] M₂
p : Submodule R M
q : Submodule R N
⊢ map₂ f (map g p) q = map₂ (f ∘ₗ g) p q
have rw : map₂ (f.flip.compl₂ g).flip p q = map₂ (f ∘ₗ g) p q
Tactic: rw [← map₂_flip, map₂_map_right, ← map₂_flip]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
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
M₂ : Type u_5
N₂ : Type u_6
inst_7 : AddCommMonoid M₂
inst_8 : AddCommMonoid N₂
inst_9 : Module R M₂
inst_10 : Module R N₂
f : M₂ →ₗ[R] N₂ →ₗ[R] P
g : M →ₗ[R] M₂
h : N →ₗ[R] N₂
p : Submodule R M
q : Submodule R N
⊢ map₂ f (map g p) (map h q) = map₂ (f.compl₁₂ g h) p q
have rw : map₂ (f.compl₂ h ∘ₗ g) p q = map₂ (f.compl₁₂ g h) p q
Tactic: rw [map₂_map_right, map₂_map_left]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Defs (goal)
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p q : Submodule R M
h : Eq.{v + 1} (α := Set M) ((fun (s : Submodule R M) ↦ s.carrier) p) ((fun (s : Submodule R M) ↦ s.carrier) q)
⊢ p = q
have mk : ∀ (toAddSubmonoid : AddSubmonoid M)
  (smul_mem' : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid.carrier → c • x ∈ toAddSubmonoid.carrier)
  (h :
    Eq.{v + 1} (α := Set M)
      ((fun (s : Submodule R M) ↦ s.carrier) { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' })
      ((fun (s : Submodule R M) ↦ s.carrier) q)),
  { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R M } = q
Tactic: cases p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Defs (goal)
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
q : Submodule R M
toAddSubmonoid : AddSubmonoid M
smul_mem' : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid.carrier → c • x ∈ toAddSubmonoid.carrier
h :
  Eq.{v + 1} (α := Set M)
    ((fun (s : Submodule R M) ↦ s.carrier) { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' })
    ((fun (s : Submodule R M) ↦ s.carrier) q)
⊢ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R M } = q
have mk : ∀ (toAddSubmonoid_1 : AddSubmonoid M)
  (smul_mem'_1 : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid_1.carrier → c • x ∈ toAddSubmonoid_1.carrier)
  (h :
    Eq.{v + 1} (α := Set M)
      ((fun (s : Submodule R M) ↦ s.carrier) { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' })
      ((fun (s : Submodule R M) ↦ s.carrier) { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 })),
  { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R M } =
    { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 }
Tactic: cases q
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Defs (goal)
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
toAddSubmonoid : AddSubmonoid M
smul_mem' : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid.carrier → c • x ∈ toAddSubmonoid.carrier
toAddSubmonoid_1 : AddSubmonoid M
smul_mem'_1 : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid_1.carrier → c • x ∈ toAddSubmonoid_1.carrier
h :
  Eq.{v + 1} (α := Set M)
    ((fun (s : Submodule R M) ↦ s.carrier) { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' })
    ((fun (s : Submodule R M) ↦ s.carrier) { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 })
⊢ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R M } =
    { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 }
have mk : toAddSubmonoid = toAddSubmonoid_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Defs (goal)
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
C : Set M
nonempty : C.Nonempty
linearComb : ∀ x ∈ C, ∀ y ∈ C, ∀ (a b : R), a • x + b • y ∈ C
⊢ 0 ∈ C
have obtain : ∀ (x : M) (hx : x ∈ C), 0 ∈ C
Tactic: obtain ⟨x, hx⟩ := nonempty
Cleared hypotheses: nonempty
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Defs (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
r : R
x : M
inst_2 : Invertible r
⊢ r • x ∈ p ↔ x ∈ p
have refine : ∀ (h : r • x ∈ p), x ∈ p
Tactic: refine ⟨fun h ↦ ?_, p.smul_mem r⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Defs (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
r : R
x : M
inst_2 : Invertible r
h : r • x ∈ p
⊢ x ∈ p
have rw : @Invertible.invOf _ MulOne.toMul MulOne.toOne r _ • r • x ∈ p
Tactic: rw [← invOf_smul_smul r x]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Defs (goal)
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
inst_2 : Semiring S
inst_3 : SMul S R
inst_4 : Module S M
inst_5 : IsScalarTower S R M
a : S
⊢ HSMul.hSMul (β := ↥p) a 0 = 0
have a₁ : (↑(HSMul.hSMul (β := ↥p) a 0) : M) = (↑0 : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Defs (goal)
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x_1 y_1 : M
inst_2 : Semiring S
inst_3 : SMul S R
inst_4 : Module S M
inst_5 : IsScalarTower S R M
a : S
x y : ↥p
⊢ a • (x + y) = a • x + a • y
have a₁ : (↑(a • (x + y)) : M) = (↑(a • x + a • y) : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Defs (goal)
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x_1 y : M
inst_2 : Semiring S
inst_3 : SMul S R
inst_4 : Module S M
inst_5 : IsScalarTower S R M
a b : S
x : ↥p
⊢ (a + b) • x = a • x + b • x
have a₁ : (↑((a + b) • x) : M) = (↑(a • x + b • x) : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Defs (goal)
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
inst_2 : Semiring S
inst_3 : SMul S R
inst_4 : Module S M
inst_5 : IsScalarTower S R M
a : ↥p
⊢ HSMul.hSMul.{u', v, v} (α := S) 0 a = 0
have a₁ : (↑(HSMul.hSMul.{u', v, v} (α := S) 0 a) : M) = (↑0 : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Defs (goal)
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
module_M : Module R M
p : Submodule R M
x y : M
hy : y ∈ p
⊢ x - y ∈ p ↔ x ∈ p
have rw : x + -y ∈ p ↔ x ∈ p
Tactic: rw [sub_eq_add_neg, p.add_mem_iff_left (p.neg_mem hy)]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Defs (goal)
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
module_M : Module R M
p : Submodule R M
x y : M
hy : y ∈ p
rw : x + -y ∈ p ↔ x ∈ p
⊢ x - y ∈ p ↔ x ∈ p
have rw₁ : x ∈ p ↔ x ∈ p
Tactic: rw [sub_eq_add_neg, p.add_mem_iff_left (p.neg_mem hy)]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Defs (goal)
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
module_M : Module R M
p : Submodule R M
x y : M
hx : x ∈ p
⊢ x - y ∈ p ↔ y ∈ p
have rw : x + -y ∈ p ↔ y ∈ p
Tactic: rw [sub_eq_add_neg, p.add_mem_iff_right hx, p.neg_mem_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Defs (goal)
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
module_M : Module R M
p : Submodule R M
x y : M
hx : x ∈ p
rw : x + -y ∈ p ↔ y ∈ p
⊢ x - y ∈ p ↔ y ∈ p
have rw₁ : -y ∈ p ↔ y ∈ p
Tactic: rw [sub_eq_add_neg, p.add_mem_iff_right hx, p.neg_mem_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Defs (goal)
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
module_M : Module R M
p : Submodule R M
x y : M
hx : x ∈ p
rw : x + -y ∈ p ↔ y ∈ p
rw₁ : -y ∈ p ↔ y ∈ p
⊢ x - y ∈ p ↔ y ∈ p
have rw₂ : y ∈ p ↔ y ∈ p
Tactic: rw [sub_eq_add_neg, p.add_mem_iff_right hx, p.neg_mem_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Defs (goal)
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module R M
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
inst_7 : SetLike T M
inst_8 : AddSubmonoidClass T M
inst_9 : SMulMemClass T R M
t : T
x x_1 : S
x_2 : ↥t
⊢ (x * x_1) • x_2 = x • x_1 • x_2
have a : (↑((x * x_1) • x_2) : M) = (↑(x • x_1 • x_2) : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Defs (goal)
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module R M
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
inst_7 : SetLike T M
inst_8 : AddSubmonoidClass T M
inst_9 : SMulMemClass T R M
t : T
x : ↥t
⊢ HSMul.hSMul.{u', v, v} (α := S) 1 x = x
have a : (↑(HSMul.hSMul.{u', v, v} (α := S) 1 x) : M) = (↑x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Defs (goal)
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module R M
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
inst_7 : SetLike T M
inst_8 : AddSubmonoidClass T M
inst_9 : SMulMemClass T R M
t : T
x : S
⊢ HSMul.hSMul (β := ↥t) x 0 = 0
have a : (↑(HSMul.hSMul (β := ↥t) x 0) : M) = (↑0 : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Defs (goal)
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module R M
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
inst_7 : SetLike T M
inst_8 : AddSubmonoidClass T M
inst_9 : SMulMemClass T R M
t : T
x : S
x_1 x_2 : ↥t
⊢ x • (x_1 + x_2) = x • x_1 + x • x_2
have a : (↑(x • (x_1 + x_2)) : M) = (↑(x • x_1 + x • x_2) : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Defs (goal)
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module R M
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
inst_7 : SetLike T M
inst_8 : AddSubmonoidClass T M
inst_9 : SMulMemClass T R M
t : T
x x_1 : S
x_2 : ↥t
⊢ (x + x_1) • x_2 = x • x_2 + x_1 • x_2
have a : (↑((x + x_1) • x_2) : M) = (↑(x • x_2 + x_1 • x_2) : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Defs (goal)
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module R M
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
inst_7 : SetLike T M
inst_8 : AddSubmonoidClass T M
inst_9 : SMulMemClass T R M
t : T
x : ↥t
⊢ HSMul.hSMul.{u', v, v} (α := S) 0 x = 0
have a : (↑(HSMul.hSMul.{u', v, v} (α := S) 0 x) : M) = (↑0 : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.EqLocus (hypothesis)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_5
inst_6 : FunLike F M M₂
inst_7 : SemilinearMapClass F τ₁₂ M M₂
f g : F
S T : Submodule R M
hS : Set.EqOn.{u_3, u_4} (β := M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) (↑S : Set M)
hT : Set.EqOn.{u_3, u_4} (β := M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) (↑T : Set M)
⊢ Set.EqOn.{u_3, u_4} (β := M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) (↑(S ⊔ T) : Set M)
have hS₁ : S ≤ eqLocus f g
Tactic: rw [← le_eqLocus] at hS hT ⊢
Cleared hypotheses: hS, hT
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.EqLocus (hypothesis)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_5
inst_6 : FunLike F M M₂
inst_7 : SemilinearMapClass F τ₁₂ M M₂
f g : F
S T : Submodule R M
hS : Set.EqOn.{u_3, u_4} (β := M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) (↑S : Set M)
hT : Set.EqOn.{u_3, u_4} (β := M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) (↑T : Set M)
hS₁ : S ≤ eqLocus f g
⊢ Set.EqOn.{u_3, u_4} (β := M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) (↑(S ⊔ T) : Set M)
have hT₁ : T ≤ eqLocus f g
Tactic: rw [← le_eqLocus] at hS hT ⊢
Cleared hypotheses: hS, hT
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Equiv (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
⊢ ofEq p p ⋯ = refl R ↥p
have h : ∀ (x : ↥p), Eq.{u_5 + 1} (α := M) (↑((ofEq p p sorry : (a : ↥p) → ↥p) x) : M) (↑((refl R ↥p : (a : ↥p) → ↥p) x) : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Equiv (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
f : M ≃ₛₗ[σ₁₂] M₂
U : Submodule R₂ M₂
⊢ (↑(f.ofSubmodule' U) : ↥(Submodule.comap (↑f : M →ₛₗ[σ₁₂] M₂) U) →ₛₗ[σ₁₂] ↥U) =
    LinearMap.codRestrict U ((↑f : M →ₛₗ[σ₁₂] M₂).domRestrict (Submodule.comap (↑f : M →ₛₗ[σ₁₂] M₂) U)) ⋯
have h : ∀ (x : ↥(Submodule.comap (↑f : M →ₛₗ[σ₁₂] M₂) U)),
  Eq.{u_7 + 1} (α := M₂)
    (↑(((↑(f.ofSubmodule' U) : ↥(Submodule.comap (↑f : M →ₛₗ[σ₁₂] M₂) U) →ₛₗ[σ₁₂] ↥U) :
            (a : ↥(Submodule.comap (↑f : M →ₛₗ[σ₁₂] M₂) U)) → ↥U)
          x) :
      M₂)
    (↑(((LinearMap.codRestrict U ((↑f : M →ₛₗ[σ₁₂] M₂).domRestrict (Submodule.comap (↑f : M →ₛₗ[σ₁₂] M₂) U)) sorry :
              LinearMap.{u_1, u_3, u_5, u_7} σ₁₂ ↥(Submodule.comap (↑f : M →ₛₗ[σ₁₂] M₂) U) ↥U) :
            (a : ↥(Submodule.comap (↑f : M →ₛₗ[σ₁₂] M₂) U)) → ↥U)
          x) :
      M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Equiv (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
p : Submodule R M
inst_4 : Module R₂ M₂
e : LinearEquiv.{u_1, u_3, u_5, u_7} σ₁₂ ↥p ↥⊥
⊢ p = ⊥
have refine : ∀ (b : M) (hb : b ∈ p), b = 0
Tactic: refine bot_unique (SetLike.le_def.2 fun b hb => (Submodule.mem_bot R).2 ?_)
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Equiv (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
p : Submodule R M
inst_4 : Module R₂ M₂
e : LinearEquiv.{u_1, u_3, u_5, u_7} σ₁₂ ↥p ↥⊥
b : M
hb : b ∈ p
⊢ b = 0
have rw : Eq.{u_7 + 1} (α := ↥⊥) ((e : (a : ↥p) → ↥⊥) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) b hb) : ↥⊥) (0 : ↥⊥)
Tactic: rw [← p.mk_eq_zero hb, ← e.map_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Equiv (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M : Module R M
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
f : M →ₛₗ[σ₁₂] M₂
g_1 : M₂ →ₛₗ[σ₂₁] M
e : M ≃ₛₗ[σ₁₂] M₂
h_1 : M₂ →ₛₗ[σ₂₃] M₃
p q : Submodule R M
inst_7 : RingHomInvPair σ₁₂ σ₂₁
inst_8 : RingHomInvPair σ₂₁ σ₁₂
g : M₂ → M
h : LeftInverse g (⇑f : (a : M) → M₂)
x : ↥f.range
x' : M
hx' : (f : (a : M) → M₂) x' = (↑x : M₂)
⊢ (f : (a : M) → M₂) (g (↑x : M₂)) = (↑x : M₂)
have rw : Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) (g ((f : (a : M) → M₂) x')) : M₂) ((f : (a : M) → M₂) x' : M₂)
Tactic: rw [← hx', h x']