awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
h' : f.ker ≤ p
rw : map p.mkQ f.ker = ⊥
⊢ (p.liftQ f h).ker = ⊥
have rw₁ : map f.ker.mkQ f.ker = ⊥
Tactic: rw [ker_liftQ, le_antisymm h h', mkQ_map_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
h' : f.ker ≤ p
rw : map p.mkQ f.ker = ⊥
rw₁ : map f.ker.mkQ f.ker = ⊥
⊢ (p.liftQ f h).ker = ⊥
have rw₂ : Eq.{u_2 + 1} (α := Submodule R (M ⧸ f.ker)) ⊥ ⊥
Tactic: rw [ker_liftQ, le_antisymm h h', mkQ_map_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
⊢ (p.mapQ q f h).range = map q.mkQ f.range
have rw : (p.liftQ (q.mkQ ∘ₛₗ f) sorry).range = map q.mkQ f.range
Tactic: rw [mapQ, range_liftQ, range_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
rw : (p.liftQ (q.mkQ ∘ₛₗ f) ⋯).range = map q.mkQ f.range
⊢ (p.mapQ q f h).range = map q.mkQ f.range
have rw₁ : (q.mkQ ∘ₛₗ f).range = map q.mkQ f.range
Tactic: rw [mapQ, range_liftQ, range_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
rw : (p.liftQ (q.mkQ ∘ₛₗ f) ⋯).range = map q.mkQ f.range
rw₁ : (q.mkQ ∘ₛₗ f).range = map q.mkQ f.range
⊢ (p.mapQ q f h).range = map q.mkQ f.range
have rw₂ : map q.mkQ f.range = map q.mkQ f.range
Tactic: rw [mapQ, range_liftQ, range_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' : Submodule R M
H : p ≤ p'
⊢ factor H ∘ₗ p.mkQ = p'.mkQ
have h : ∀ (x : M), Eq (α := M ⧸ p') ((factor H ∘ₗ p.mkQ : (a : M) → M ⧸ p') x : M ⧸ p') ((p'.mkQ : (a : M) → M ⧸ p') x : M ⧸ p')
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' : Submodule R M
H : p ≤ p'
x : M
⊢ Eq (α := M ⧸ p') ((factor H ∘ₗ p.mkQ : (a : M) → M ⧸ p') x : M ⧸ p') ((p'.mkQ : (a : M) → M ⧸ p') x : M ⧸ p')
have h : Eq (α := M ⧸ p') ((factor H : (a : M ⧸ p) → M ⧸ p') ((p.mkQ : (a : M) → M ⧸ p) x) : M ⧸ p')
  ((p'.mkQ : (a : M) → M ⧸ p') x : M ⧸ p')
Tactic: rw [LinearMap.comp_apply, factor_mk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' : Submodule R M
H : p ≤ p'
x : M
h :
  Eq (α := M ⧸ p') ((factor H : (a : M ⧸ p) → M ⧸ p') ((p.mkQ : (a : M) → M ⧸ p) x) : M ⧸ p')
    ((p'.mkQ : (a : M) → M ⧸ p') x : M ⧸ p')
⊢ Eq (α := M ⧸ p') ((factor H ∘ₗ p.mkQ : (a : M) → M ⧸ p') x : M ⧸ p') ((p'.mkQ : (a : M) → M ⧸ p') x : M ⧸ p')
have h₁ : Eq (α := M ⧸ p') ((p'.mkQ : (a : M) → M ⧸ p') x : M ⧸ p') ((p'.mkQ : (a : M) → M ⧸ p') x : M ⧸ p')
Tactic: rw [LinearMap.comp_apply, factor_mk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' p'' : Submodule R M
H1 : p ≤ p'
H2 : p' ≤ p''
⊢ factor H2 ∘ₗ factor H1 = factor ⋯
have h : ∀ (x : M),
  Eq (α := M ⧸ p'') (((factor H2 ∘ₗ factor H1) ∘ₗ p.mkQ : (a : M) → M ⧸ p'') x : M ⧸ p'')
    ((factor sorry ∘ₗ p.mkQ : (a : M) → M ⧸ p'') x : M ⧸ p'')
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' p'' : Submodule R M
H1 : p ≤ p'
H2 : p' ≤ p''
x : M ⧸ p
⊢ Eq (α := M ⧸ p'') ((factor H2 : (a : M ⧸ p') → M ⧸ p'') ((factor H1 : (a : M ⧸ p) → M ⧸ p') x) : M ⧸ p'')
    ((factor ⋯ : (a : M ⧸ p) → M ⧸ p'') x : M ⧸ p'')
have rw : Eq (α := M ⧸ p'') ((factor H2 ∘ₗ factor H1 : (a : M ⧸ p) → M ⧸ p'') x : M ⧸ p'')
  ((factor sorry : (a : M ⧸ p) → M ⧸ p'') x : M ⧸ p'')
Tactic: rw [← comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' : Submodule R M
H : p ≤ p'
x : M ⧸ p'
⊢ ∃ (a : M ⧸ p), (factor H : (a : M ⧸ p) → M ⧸ p') a = x
have h : (factor H : (a : M ⧸ p) → M ⧸ p') (Quotient.mk (Quotient.out x)) = x
Tactic: use Quotient.mk x.out
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ (↑f.range : Set M₂)
⊢ span R ((⇑f : (a : M) → M₂) ⁻¹' s) = comap f (span R₂ s)
have suffices : comap f (span R₂ s) ≤ span R ((⇑f : (a : M) → M₂) ⁻¹' s)
Tactic: suffices (span R₂ s).comap f ≤ span R (f ⁻¹' s) by exact le_antisymm (span_preimage_le f s) this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ (↑f.range : Set M₂)
y : M₂ := Classical.choose (p := Membership.mem s) h₀
⊢ f.ker ≤ span R ((⇑f : (a : M) → M₂) ⁻¹' s)
have hy : y ∈ s
Tactic: have hy : y ∈ s := Classical.choose_spec h₀
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ (↑f.range : Set M₂)
y : M₂ := Classical.choose (p := Membership.mem s) h₀
hy : y ∈ s
⊢ f.ker ≤ span R ((⇑f : (a : M) → M₂) ⁻¹' s)
have rw : ∃ y ∈ f.range, Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑(span R ((⇑f : (a : M) → M₂) ⁻¹' s)) : Set M)
Tactic: rw [ker_le_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ (↑f.range : Set M₂)
y : M₂ := Classical.choose (p := Membership.mem s) h₀
hy : y ∈ s
⊢ ∃ y ∈ f.range, Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑(span R ((⇑f : (a : M) → M₂) ⁻¹' s)) : Set M)
have right : Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑(span R ((⇑f : (a : M) → M₂) ⁻¹' s)) : Set M)
Tactic: use y, h₁ hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ (↑f.range : Set M₂)
y : M₂ := Classical.choose (p := Membership.mem s) h₀
hy : y ∈ s
⊢ Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑(span R ((⇑f : (a : M) → M₂) ⁻¹' s)) : Set M)
have hy₁ : {y} ⊆ s
Tactic: rw [← Set.singleton_subset_iff] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ (↑f.range : Set M₂)
⊢ comap f (span R₂ s) ≤ span R ((⇑f : (a : M) → M₂) ⁻¹' s)
have hk : f.ker ≤ span R ((⇑f : (a : M) → M₂) ⁻¹' s)
Tactic: have hk : ker f ≤ span R (f ⁻¹' s) := by
    let y := Classical.choose h₀
    have hy : y ∈ s := Classical.choose_spec h₀
    rw [ker_le_iff]
    use y, h₁ hy
    rw [← Set.singleton_subset_iff] at hy
    exact Set.Subset.trans subset_span (span_mono (Set.preimage_mono hy))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ (↑f.range : Set M₂)
hk : f.ker ≤ span R ((⇑f : (a : M) → M₂) ⁻¹' s)
⊢ comap f (span R₂ s) ≤ span R ((⇑f : (a : M) → M₂) ⁻¹' s)
have hk₁ : span R ((⇑f : (a : M) → M₂) ⁻¹' s) = span R ((⇑f : (a : M) → M₂) ⁻¹' s) ⊔ f.ker
Tactic: rw [← left_eq_sup] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ (↑f.range : Set M₂)
hk : span R ((⇑f : (a : M) → M₂) ⁻¹' s) = span R ((⇑f : (a : M) → M₂) ⁻¹' s) ⊔ f.ker
⊢ comap f (span R₂ s) ≤ span R ((⇑f : (a : M) → M₂) ⁻¹' s)
have h₂ : s ⊆ Set.range.{u_4, u_2 + 1} (ι := M) (⇑f : (a : M) → M₂)
Tactic: rw [coe_range f] at h₁
Cleared hypotheses: h₁, hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ Set.range.{u_4, u_2 + 1} (ι := M) (⇑f : (a : M) → M₂)
hk : span R ((⇑f : (a : M) → M₂) ⁻¹' s) = span R ((⇑f : (a : M) → M₂) ⁻¹' s) ⊔ f.ker
⊢ comap f (span R₂ s) ≤ span R ((⇑f : (a : M) → M₂) ⁻¹' s)
have rw : f.range ⊓ span R₂ s ≤ span R₂ s
Tactic: rw [hk, ← LinearMap.map_le_map_iff, map_span, map_comap_eq, Set.image_preimage_eq_of_subset h₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_2
r : R
x_1 y : M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' p'' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
N : Type u_5
inst_6 : AddCommGroup N
inst_7 : Module R N
P : Submodule R M
Q : Submodule R N
f : M ≃ₗ[R] N
hf : map (↑f : M →ₗ[R] N) P = Q
x : N
hx : x ∈ Q
⊢ x ∈ comap (↑f.symm : N →ₗ[R] M) P
have hx₁ : ∃ y ∈ P, ((↑f : M →ₗ[R] N) : (a : M) → N) y = x
Tactic: rw [← hf, Submodule.mem_map] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
r : R
x_1 y : M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' p'' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
N : Type u_5
inst_6 : AddCommGroup N
inst_7 : Module R N
P : Submodule R M
Q : Submodule R N
f : M ≃ₗ[R] N
hf : map (↑f : M →ₗ[R] N) P = Q
x : N
hx : ∃ y ∈ P, ((↑f : M →ₗ[R] N) : (a : M) → N) y = x
⊢ x ∈ comap (↑f.symm : N →ₗ[R] M) P
have obtain : ∀ (y : M) (hy : y ∈ P), Membership.mem (α := N) (comap (↑f.symm : N →ₗ[R] M) P) (((↑f : M →ₗ[R] N) : (a : M) → N) y : N)
Tactic: obtain ⟨y, hy, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
O : Type u_6
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup O
inst_6 : Module R O
P : Submodule R M
Q : Submodule R N
S : Submodule R O
e : M ≃ₗ[R] N
f : N ≃ₗ[R] O
he : map (↑e : M →ₗ[R] N) P = Q
hf : map (↑f : N →ₗ[R] O) Q = S
hef : map (↑(e ≪≫ₗ f) : M →ₗ[R] O) P = S
⊢ equiv P S (e ≪≫ₗ f) hef = equiv P Q e he ≪≫ₗ equiv Q S f hf
have h : ∀ (x : M ⧸ P),
  Eq.{u_6 + 1} (α := O ⧸ S) ((equiv P S (e ≪≫ₗ f) hef : (a : M ⧸ P) → O ⧸ S) x : O ⧸ S)
    (((equiv P Q e he ≪≫ₗ equiv Q S f hf : LinearEquiv.{u_1, u_1, u_2, u_6} (RingHom.id R) (M ⧸ P) (O ⧸ S)) :
          (a : M ⧸ P) → O ⧸ S)
        x :
      O ⧸ S)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
O : Type u_6
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup O
inst_6 : Module R O
P : Submodule R M
Q : Submodule R N
S : Submodule R O
e : M ≃ₗ[R] N
f : N ≃ₗ[R] O
he : map (↑e : M →ₗ[R] N) P = Q
hf : map (↑f : N →ₗ[R] O) Q = S
hef : map (↑(e ≪≫ₗ f) : M →ₗ[R] O) P = S
x : M ⧸ P
⊢ Eq.{u_6 + 1} (α := O ⧸ S) ((equiv P S (e ≪≫ₗ f) hef : (a : M ⧸ P) → O ⧸ S) x : O ⧸ S)
    (((equiv P Q e he ≪≫ₗ equiv Q S f hf : LinearEquiv.{u_1, u_1, u_2, u_6} (RingHom.id R) (M ⧸ P) (O ⧸ S)) :
          (a : M ⧸ P) → O ⧸ S)
        x :
      O ⧸ S)
have h : Eq.{u_6 + 1} (α := O ⧸ S) ((P.mapQ S ((↑f : N →ₗ[R] O) ∘ₗ (↑e : M →ₗ[R] N)) sorry : (a : M ⧸ P) → O ⧸ S) x : O ⧸ S)
  ((Q.mapQ S (↑f : N →ₗ[R] O) sorry : (a : N ⧸ Q) → O ⧸ S) ((P.mapQ Q (↑e : M →ₗ[R] N) sorry : (a : M ⧸ P) → N ⧸ Q) x) : O ⧸ S)
Tactic: simp only [Quotient.equiv_apply, LinearEquiv.trans_apply, LinearEquiv.coe_trans]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
O : Type u_6
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup O
inst_6 : Module R O
P : Submodule R M
Q : Submodule R N
S : Submodule R O
e : M ≃ₗ[R] N
f : N ≃ₗ[R] O
he : map (↑e : M →ₗ[R] N) P = Q
hf : map (↑f : N →ₗ[R] O) Q = S
hef : map (↑(e ≪≫ₗ f) : M →ₗ[R] O) P = S
x : M ⧸ P
⊢ Eq.{u_6 + 1} (α := O ⧸ S) ((P.mapQ S ((↑f : N →ₗ[R] O) ∘ₗ (↑e : M →ₗ[R] N)) ⋯ : (a : M ⧸ P) → O ⧸ S) x : O ⧸ S)
    ((Q.mapQ S (↑f : N →ₗ[R] O) ⋯ : (a : N ⧸ Q) → O ⧸ S) ((P.mapQ Q (↑e : M →ₗ[R] N) ⋯ : (a : M ⧸ P) → N ⧸ Q) x) :
      O ⧸ S)
have h : Eq.{u_6 + 1} (α := O ⧸ S) ((Q.mapQ S (↑f : N →ₗ[R] O) sorry ∘ₗ P.mapQ Q (↑e : M →ₗ[R] N) sorry : (a : M ⧸ P) → O ⧸ S) x : O ⧸ S)
  ((Q.mapQ S (↑f : N →ₗ[R] O) sorry : (a : N ⧸ Q) → O ⧸ S) ((P.mapQ Q (↑e : M →ₗ[R] N) sorry : (a : M ⧸ P) → N ⧸ Q) x) : O ⧸ S)
Tactic: rw [mapQ_comp, LinearMap.comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
O : Type u_6
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup O
inst_6 : Module R O
P : Submodule R M
Q : Submodule R N
S : Submodule R O
e : M ≃ₗ[R] N
f : N ≃ₗ[R] O
he : map (↑e : M →ₗ[R] N) P = Q
hf : map (↑f : N →ₗ[R] O) Q = S
hef : map (↑(e ≪≫ₗ f) : M →ₗ[R] O) P = S
x : M ⧸ P
h :
  Eq.{u_6 + 1} (α := O ⧸ S)
    ((Q.mapQ S (↑f : N →ₗ[R] O) ⋯ ∘ₗ P.mapQ Q (↑e : M →ₗ[R] N) ⋯ : (a : M ⧸ P) → O ⧸ S) x : O ⧸ S)
    ((Q.mapQ S (↑f : N →ₗ[R] O) ⋯ : (a : N ⧸ Q) → O ⧸ S) ((P.mapQ Q (↑e : M →ₗ[R] N) ⋯ : (a : M ⧸ P) → N ⧸ Q) x) :
      O ⧸ S)
h₁ : Submodule R N
⊢ Eq.{u_6 + 1} (α := O ⧸ S) ((P.mapQ S ((↑f : N →ₗ[R] O) ∘ₗ (↑e : M →ₗ[R] N)) ⋯ : (a : M ⧸ P) → O ⧸ S) x : O ⧸ S)
    ((Q.mapQ S (↑f : N →ₗ[R] O) ⋯ : (a : N ⧸ Q) → O ⧸ S) ((P.mapQ Q (↑e : M →ₗ[R] N) ⋯ : (a : M ⧸ P) → N ⧸ Q) x) :
      O ⧸ S)
have h₂ : P ≤ comap (↑e : M →ₗ[R] N) Q
Tactic: rw [mapQ_comp, LinearMap.comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
O : Type u_6
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup O
inst_6 : Module R O
P : Submodule R M
Q : Submodule R N
S : Submodule R O
e : M ≃ₗ[R] N
f : N ≃ₗ[R] O
he : map (↑e : M →ₗ[R] N) P = Q
hf : map (↑f : N →ₗ[R] O) Q = S
hef : map (↑(e ≪≫ₗ f) : M →ₗ[R] O) P = S
x : M ⧸ P
h :
  Eq.{u_6 + 1} (α := O ⧸ S)
    ((Q.mapQ S (↑f : N →ₗ[R] O) ⋯ ∘ₗ P.mapQ Q (↑e : M →ₗ[R] N) ⋯ : (a : M ⧸ P) → O ⧸ S) x : O ⧸ S)
    ((Q.mapQ S (↑f : N →ₗ[R] O) ⋯ : (a : N ⧸ Q) → O ⧸ S) ((P.mapQ Q (↑e : M →ₗ[R] N) ⋯ : (a : M ⧸ P) → N ⧸ Q) x) :
      O ⧸ S)
h₁ : Submodule R N
h₂ : P ≤ comap (↑e : M →ₗ[R] N) Q
⊢ Eq.{u_6 + 1} (α := O ⧸ S) ((P.mapQ S ((↑f : N →ₗ[R] O) ∘ₗ (↑e : M →ₗ[R] N)) ⋯ : (a : M ⧸ P) → O ⧸ S) x : O ⧸ S)
    ((Q.mapQ S (↑f : N →ₗ[R] O) ⋯ : (a : N ⧸ Q) → O ⧸ S) ((P.mapQ Q (↑e : M →ₗ[R] N) ⋯ : (a : M ⧸ P) → N ⧸ Q) x) :
      O ⧸ S)
have h₃ : Q ≤ comap (↑f : N →ₗ[R] O) S
Tactic: rw [mapQ_comp, LinearMap.comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
O : Type u_6
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup O
inst_6 : Module R O
P : Submodule R M
Q : Submodule R N
S : Submodule R O
e : M ≃ₗ[R] N
f : N ≃ₗ[R] O
he : map (↑e : M →ₗ[R] N) P = Q
hf : map (↑f : N →ₗ[R] O) Q = S
hef : map (↑(e ≪≫ₗ f) : M →ₗ[R] O) P = S
x : M ⧸ P
h :
  Eq.{u_6 + 1} (α := O ⧸ S)
    ((Q.mapQ S (↑f : N →ₗ[R] O) ⋯ ∘ₗ P.mapQ Q (↑e : M →ₗ[R] N) ⋯ : (a : M ⧸ P) → O ⧸ S) x : O ⧸ S)
    ((Q.mapQ S (↑f : N →ₗ[R] O) ⋯ : (a : N ⧸ Q) → O ⧸ S) ((P.mapQ Q (↑e : M →ₗ[R] N) ⋯ : (a : M ⧸ P) → N ⧸ Q) x) :
      O ⧸ S)
h₁ : Submodule R N
h₂ : P ≤ comap (↑e : M →ₗ[R] N) Q
h₃ : Q ≤ comap (↑f : N →ₗ[R] O) S
⊢ Eq.{u_6 + 1} (α := O ⧸ S) ((P.mapQ S ((↑f : N →ₗ[R] O) ∘ₗ (↑e : M →ₗ[R] N)) ⋯ : (a : M ⧸ P) → O ⧸ S) x : O ⧸ S)
    ((Q.mapQ S (↑f : N →ₗ[R] O) ⋯ : (a : N ⧸ Q) → O ⧸ S) ((P.mapQ Q (↑e : M →ₗ[R] N) ⋯ : (a : M ⧸ P) → N ⧸ Q) x) :
      O ⧸ S)
have h₄ : Eq.{u_6 + 1} (α := O ⧸ S)
  ((Q.mapQ S (↑f : N →ₗ[R] O) sorry : (a : N ⧸ Q) → O ⧸ S) ((P.mapQ Q (↑e : M →ₗ[R] N) sorry : (a : M ⧸ P) → N ⧸ Q) x) : O ⧸ S)
  ((Q.mapQ S (↑f : N →ₗ[R] O) sorry : (a : N ⧸ Q) → O ⧸ S) ((P.mapQ Q (↑e : M →ₗ[R] N) sorry : (a : M ⧸ P) → N ⧸ Q) x) : O ⧸ S)
Tactic: rw [mapQ_comp, LinearMap.comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
R₃ : Type u_5
M₃ : Type u_6
inst : Ring R
inst_1 : Ring R₂
inst_2 : Ring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommGroup M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
inst_9 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
⊢ g.ker ≤ f.range ↔ f.range.mkQ ∘ₗ g.ker.subtype = 0
have rw : g.ker ≤ f.range ↔ g.ker.subtype.range ≤ f.range.mkQ.ker
Tactic: rw [← range_le_ker_iff, Submodule.ker_mkQ, Submodule.range_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
R₃ : Type u_5
M₃ : Type u_6
inst : Ring R
inst_1 : Ring R₂
inst_2 : Ring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommGroup M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
inst_9 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
rw : g.ker ≤ f.range ↔ g.ker.subtype.range ≤ f.range.mkQ.ker
⊢ g.ker ≤ f.range ↔ f.range.mkQ ∘ₗ g.ker.subtype = 0
have rw₁ : g.ker ≤ f.range ↔ g.ker.subtype.range ≤ f.range
Tactic: rw [← range_le_ker_iff, Submodule.ker_mkQ, Submodule.range_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
R₃ : Type u_5
M₃ : Type u_6
inst : Ring R
inst_1 : Ring R₂
inst_2 : Ring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommGroup M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
inst_9 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
rw : g.ker ≤ f.range ↔ g.ker.subtype.range ≤ f.range.mkQ.ker
rw₁ : g.ker ≤ f.range ↔ g.ker.subtype.range ≤ f.range
⊢ g.ker ≤ f.range ↔ f.range.mkQ ∘ₗ g.ker.subtype = 0
have rw₂ : g.ker ≤ f.range ↔ g.ker ≤ f.range
Tactic: rw [← range_le_ker_iff, Submodule.ker_mkQ, Submodule.range_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ f.range), u ∘ₛₗ f = v ∘ₛₗ f → u = v
⊢ f.range = ⊤
have h₁ : Eq (α := LinearMap.{u_1, u_3, u_2, u_4} τ₁₂ M (M₂ ⧸ f.range)) (comp (σ₂₃ := RingHom.id R₂) 0 f) 0
Tactic: have h₁ : (0 : M₂ →ₗ[R₂] M₂ ⧸ (range f)).comp f = 0 := zero_comp _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ f.range), u ∘ₛₗ f = v ∘ₛₗ f → u = v
h₁ : Eq (α := LinearMap.{u_1, u_3, u_2, u_4} τ₁₂ M (M₂ ⧸ f.range)) (comp (σ₂₃ := RingHom.id R₂) 0 f) 0
⊢ f.range = ⊤
have rw : Eq.{u_4 + 1} (α := Submodule R₂ M₂) (ker (R₂ := R₂) (M₂ := M₂ ⧸ f.range) (τ₁₂ := RingHom.id R₂) 0) ⊤
Tactic: rw [← Submodule.ker_mkQ (range f), ← h 0 (range f).mkQ (Eq.trans h₁ (range_mkQ_comp _).symm)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
r : R
x_1 y_1 : M
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
p : Submodule R M
q : Submodule R M₂
x y : ↥(p.compatibleMaps q)
⊢ p.mapQ q (↑(x + y) : M →ₗ[R] M₂) ⋯ = p.mapQ q (↑x : M →ₗ[R] M₂) ⋯ + p.mapQ q (↑y : M →ₗ[R] M₂) ⋯
have h : ∀ (x_2 : M),
  Eq.{u_3 + 1} (α := M₂ ⧸ q) ((p.mapQ q (↑(x + y) : M →ₗ[R] M₂) sorry ∘ₗ p.mkQ : (a : M) → M₂ ⧸ q) x_2 : M₂ ⧸ q)
    (((p.mapQ q (↑x : M →ₗ[R] M₂) sorry + p.mapQ q (↑y : M →ₗ[R] M₂) sorry) ∘ₗ p.mkQ : (a : M) → M₂ ⧸ q) x_2 : M₂ ⧸ q)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
r : R
x y : M
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
p : Submodule R M
q : Submodule R M₂
c : R
f : ↥(p.compatibleMaps q)
⊢ p.mapQ q (↑(c • f) : M →ₗ[R] M₂) ⋯ =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (p.mapQ q (↑f : M →ₗ[R] M₂) ⋯)
have h : ∀ (x : M),
  Eq.{u_3 + 1} (α := M₂ ⧸ q) ((p.mapQ q (↑(c • f) : M →ₗ[R] M₂) sorry ∘ₗ p.mkQ : (a : M) → M₂ ⧸ q) x : M₂ ⧸ q)
    ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (p.mapQ q (↑f : M →ₗ[R] M₂) sorry) ∘ₗ p.mkQ :
          (a : M) → M₂ ⧸ q)
        x :
      M₂ ⧸ q)
Tactic: ext