awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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₀
⊢ y ∈ s

Tactic:
have hy : y ∈ s := Classical.choose_spec h₀
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
rw : ∃ y ∈ f.range, Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑(span R ((⇑f : (a : M) → M₂) ⁻¹' s)) : Set M)
⊢ f.ker ≤ span R ((⇑f : (a : M) → M₂) ⁻¹' s)

Tactic:
rw [ker_le_iff]

Premises used: LinearMap.ker_le_iff
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
right : Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑(span R ((⇑f : (a : M) → M₂) ⁻¹' s)) : Set M)
⊢ ∃ y ∈ f.range, Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑(span R ((⇑f : (a : M) → M₂) ⁻¹' s)) : Set M)

Tactic:
use y, h₁ hy
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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} ⊆ s

Tactic:
rw [← Set.singleton_subset_iff] at hy

Premises used: Set.singleton_subset_iff
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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)

Tactic:
Set.Subset.trans subset_span (span_mono (Set.preimage_mono hy))

Premises used: Set.Subset.trans, Set.preimage_mono, Submodule.span_mono, Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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)

Tactic:
exact Set.Subset.trans subset_span (span_mono (Set.preimage_mono hy))

Premises used: Set.Subset.trans, Set.preimage_mono, Submodule.span_mono, Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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₂)
⊢ 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))
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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)
⊢ span R ((⇑f : (a : M) → M₂) ⁻¹' s) = span R ((⇑f : (a : M) → M₂) ⁻¹' s) ⊔ f.ker

Tactic:
rw [← left_eq_sup] at hk

Premises used: left_eq_sup
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
⊢ s ⊆ Set.range.{u_4, u_2 + 1} (ι := M) (⇑f : (a : M) → M₂)

Tactic:
rw [coe_range f] at h₁

Premises used: LinearMap.coe_range
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
h₂ : s ⊆ Set.range.{u_4, u_2 + 1} (ι := M) (⇑f : (a : M) → M₂)
⊢ span R ((⇑f : (a : M) → M₂) ⁻¹' s) = span R ((⇑f : (a : M) → M₂) ⁻¹' s) ⊔ f.ker

Tactic:
rw [coe_range f] at h₁

Premises used: LinearMap.coe_range
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
rw : f.range ⊓ span R₂ s ≤ span R₂ s
⊢ comap f (span R₂ s) ≤ span R ((⇑f : (a : M) → M₂) ⁻¹' s)

Tactic:
rw [hk, ← LinearMap.map_le_map_iff, map_span, map_comap_eq, Set.image_preimage_eq_of_subset h₁]

Premises used: LinearMap.map_le_map_iff, Submodule.map_comap_eq, Set.image_preimage_eq_of_subset, Submodule.map_span
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
⊢ f.range ⊓ span R₂ s ≤ span R₂ s

Tactic:
inf_le_right

Premises used: Set.Mem, inf_le_right
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
⊢ f.range ⊓ span R₂ s ≤ span R₂ s

Tactic:
exact inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
⊢ ∃ y ∈ P, ((↑f : M →ₗ[R] N) : (a : M) → N) y = x

Tactic:
rw [← hf, Submodule.mem_map] at hx

Premises used: Submodule.mem_map
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
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)
⊢ x ∈ comap (↑f.symm : N →ₗ[R] M) P

Tactic:
obtain ⟨y, hy, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
Goal:
R : Type u_1
M : Type u_2
r : R
x y_1 : 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
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:
simpa
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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 : M ⧸ P
⊢ ∀ (z : M),
    Eq.{u_2 + 1} (α := M ⧸ P)
      ((Q.mapQ P (↑f.symm : N →ₗ[R] M) ⋯ : (a : N ⧸ Q) → M ⧸ P)
          ((P.mapQ Q (↑f : M →ₗ[R] N) ⋯ : (a : M ⧸ P) → N ⧸ Q) (mk z)) :
        M ⧸ P)
      (mk z : M ⧸ P)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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 ⧸ Q
⊢ ∀ (z : N),
    Eq.{u_5 + 1} (α := N ⧸ Q)
      ((P.mapQ Q (↑f : M →ₗ[R] N) ⋯ : (a : M ⧸ P) → N ⧸ Q)
          ((Q.mapQ P (↑f.symm : N →ₗ[R] M) ⋯ : (a : N ⧸ Q) → M ⧸ P) (mk z)) :
        N ⧸ Q)
      (mk z : N ⧸ Q)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
Goal:
R : Type u_5
M : Type u_6
N : Type u_7
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : Submodule R M
Q : Submodule R N
f : M ≃ₗ[R] N
hf : map (↑f : M →ₗ[R] N) P = Q
⊢ (equiv P Q f hf).symm = equiv Q P f.symm ⋯

Tactic:
rfl

Premises used: LinearEquiv.symm, Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.equiv, Submodule.quotientRel, AddAction.orbitRel, AddCon.Quotient, rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
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)
⊢ equiv P S (e ≪≫ₗ f) hef = equiv P Q e he ≪≫ₗ equiv Q S f hf

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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) ((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)
⊢ 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:
simp only [Quotient.equiv_apply, LinearEquiv.trans_apply, LinearEquiv.coe_trans]

Premises used: LinearEquiv.trans_apply, LinearEquiv.coe_trans, Submodule.Quotient.equiv_apply
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
h₄ :
  Eq.{u_6 + 1} (α := 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)
    ((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
h₈ :
  Eq.{u_6 + 1} (α := 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)
    ((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)

Tactic:
rw [mapQ_comp, LinearMap.comp_apply]

Premises used: Submodule.comap_mono, LinearMap.comp_apply, LE.le.trans, Submodule.mapQ_comp
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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₂
x : M
⊢ Eq.{u_4 + 1} (α := M₂ ⧸ f.range) ((f.range.mkQ ∘ₛₗ f : (a : M) → M₂ ⧸ f.range) x : M₂ ⧸ f.range)
    (((0 : LinearMap.{u_1, u_3, u_2, u_4} τ₁₂ M (M₂ ⧸ f.range)) : (a : M) → M₂ ⧸ f.range) x : M₂ ⧸ f.range)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
rw₂ rw₃ : g.ker ≤ f.range ↔ g.ker ≤ f.range
⊢ g.ker ≤ f.range ↔ f.range.mkQ ∘ₗ g.ker.subtype = 0

Tactic:
rw [← range_le_ker_iff, Submodule.ker_mkQ, Submodule.range_subtype]

Premises used: Submodule.ker_mkQ, Submodule.range_subtype, LinearMap.range_le_ker_iff
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
⊢ 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 _
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
rw : Eq.{u_4 + 1} (α := Submodule R₂ M₂) (ker (R₂ := R₂) (M₂ := M₂ ⧸ f.range) (τ₁₂ := RingHom.id R₂) 0) ⊤
⊢ f.range = ⊤

Tactic:
rw [← Submodule.ker_mkQ (range f), ← h 0 (range f).mkQ (Eq.trans h₁ (range_mkQ_comp _).symm)]

Premises used: LinearMap.range_mkQ_comp, LinearMap.range, Submodule.mkQ, Submodule.ker_mkQ, OfNat.ofNat, Eq.symm, Eq.trans
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
⊢ Eq.{u_4 + 1} (α := Submodule R₂ M₂) (ker (R₂ := R₂) (M₂ := M₂ ⧸ f.range) (τ₁₂ := RingHom.id R₂) 0) ⊤

Tactic:
ker_zero

Premises used: LinearMap.ker_zero
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
⊢ Eq.{u_4 + 1} (α := Submodule R₂ M₂) (ker (R₂ := R₂) (M₂ := M₂ ⧸ f.range) (τ₁₂ := RingHom.id R₂) 0) ⊤

Tactic:
exact ker_zero

Premises used: LinearMap.ker_zero
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
hp : p = ⊥
x : M
⊢ (p.quotEquivOfEqBot hp : (a : M ⧸ p) → M) (Quotient.mk x) = x

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
hp : p = ⊥
x : M
⊢ Eq (α := M ⧸ p) (((p.quotEquivOfEqBot hp).symm : (a : M) → M ⧸ p) x : M ⧸ p) (Quotient.mk x : M ⧸ p)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
hp : p = ⊥
⊢ (↑(p.quotEquivOfEqBot hp).symm : M →ₗ[R] M ⧸ p) = p.mkQ

Tactic:
rfl

Premises used: Submodule.Quotient.mk, Submodule.mkQ, rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
Goal:
R : Type u_1
M : Type u_2
r : R
x y : M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' P Q : Submodule R M
hf : map (↑(LinearEquiv.refl R M) : M →ₗ[R] M) P = Q
⊢ P = Q

Tactic:
simpa using hf
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
P Q : Submodule R M
hf : map (↑(LinearEquiv.refl R M) : M →ₗ[R] M) P = Q
⊢ equiv P Q (LinearEquiv.refl R M) hf = P.quotEquivOfEq Q ⋯

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, Submodule.Quotient.equiv, Quotient, Quot.map, Submodule.quotEquivOfEq, AddCon.Quotient, rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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)
h :
  ∀ (x_2 : M),
    Eq.{u_3 + 1} (α := M₂ ⧸ q) ((p.mapQ q (↑(x + y) : M →ₗ[R] M₂) ⋯ ∘ₗ p.mkQ : (a : M) → M₂ ⧸ q) x_2 : M₂ ⧸ q)
      (((p.mapQ q (↑x : M →ₗ[R] M₂) ⋯ + p.mapQ q (↑y : M →ₗ[R] M₂) ⋯) ∘ₗ p.mkQ : (a : M) → M₂ ⧸ q) x_2 : M₂ ⧸ q)
⊢ p.mapQ q (↑(x + y) : M →ₗ[R] M₂) ⋯ = p.mapQ q (↑x : M →ₗ[R] M₂) ⋯ + p.mapQ q (↑y : M →ₗ[R] M₂) ⋯

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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)
x_2 : M
⊢ Eq.{u_3 + 1} (α := M₂ ⧸ q) ((p.mapQ q (↑(x + y) : M →ₗ[R] M₂) ⋯ ∘ₗ p.mkQ : (a : M) → M₂ ⧸ q) x_2 : M₂ ⧸ q)
    (((p.mapQ q (↑x : M →ₗ[R] M₂) ⋯ + p.mapQ q (↑y : M →ₗ[R] M₂) ⋯) ∘ₗ p.mkQ : (a : M) → M₂ ⧸ q) x_2 : M₂ ⧸ q)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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)
h :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := M₂ ⧸ q) ((p.mapQ q (↑(c • f) : M →ₗ[R] M₂) ⋯ ∘ₗ 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₂) ⋯) ∘ₗ p.mkQ :
            (a : M) → M₂ ⧸ q)
          x :
        M₂ ⧸ 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₂) ⋯)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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)
x_1 : M
⊢ Eq.{u_3 + 1} (α := M₂ ⧸ q) ((p.mapQ q (↑(c • f) : M →ₗ[R] M₂) ⋯ ∘ₗ p.mkQ : (a : M) → M₂ ⧸ q) x_1 : M₂ ⧸ q)
    ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (p.mapQ q (↑f : M →ₗ[R] M₂) ⋯) ∘ₗ p.mkQ :
          (a : M) → M₂ ⧸ q)
        x_1 :
      M₂ ⧸ q)

Tactic:
rfl