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
p p' : Submodule R M
⊢ map p.mkQ p' = ⊤ ↔ p ⊔ p' = ⊤

Tactic:
simp only [LinearMap.map_eq_top_iff p.range_mkQ, sup_comm, ker_mkQ]

Premises used: Submodule.range_mkQ, sup_comm, Submodule.ker_mkQ, LinearMap.map_eq_top_iff
-- 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'' : 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₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
⊢ p ≤ (q.mkQ ∘ₛₗ f).ker

Tactic:
simpa [ker_comp] using h

Premises used: LinearMap.ker_comp
-- 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
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₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
x : M
⊢ Eq.{u_4 + 1} (α := M₂ ⧸ q) ((p.mapQ q f h : (a : M ⧸ p) → M₂ ⧸ q) (Quotient.mk x) : M₂ ⧸ q)
    (Quotient.mk ((f : (a : M) → M₂) x) : M₂ ⧸ q)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, 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
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₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
h₁ :
  ∀ (x : M),
    Eq.{u_4 + 1} (α := M₂ ⧸ q) ((p.mapQ q f h ∘ₛₗ p.mkQ : (a : M) → M₂ ⧸ q) x : M₂ ⧸ q)
      ((q.mkQ ∘ₛₗ f : (a : M) → M₂ ⧸ q) x : M₂ ⧸ q)
⊢ p.mapQ q f h ∘ₛₗ p.mkQ = q.mkQ ∘ₛₗ f

Tactic:
ext x
-- 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
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₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
x : M
⊢ Eq.{u_4 + 1} (α := M₂ ⧸ q) ((p.mapQ q f h ∘ₛₗ p.mkQ : (a : M) → M₂ ⧸ q) x : M₂ ⧸ q)
    ((q.mkQ ∘ₛₗ f : (a : M) → M₂ ⧸ q) x : M₂ ⧸ q)

Tactic:
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'' : 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₂
⊢ p ≤ comap (σ₁₂ := τ₁₂) 0 q

Tactic:
simp
-- 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
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₂
h : p ≤ comap (σ₁₂ := τ₁₂) 0 q
h₁ :
  ∀ (x : M),
    Eq.{u_4 + 1} (α := M₂ ⧸ q) ((p.mapQ q 0 h ∘ₛₗ p.mkQ : (a : M) → M₂ ⧸ q) x : M₂ ⧸ q)
      ((comp (σ₂₃ := τ₁₂) 0 p.mkQ : (a : M) → M₂ ⧸ q) x : M₂ ⧸ q)
⊢ p.mapQ q 0 h = 0

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
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₂
h : p ≤ comap (σ₁₂ := τ₁₂) 0 q
x : M
⊢ Eq.{u_4 + 1} (α := M₂ ⧸ q) ((p.mapQ q 0 h ∘ₛₗ p.mkQ : (a : M) → M₂ ⧸ q) x : M₂ ⧸ q)
    ((comp (σ₂₃ := τ₁₂) 0 p.mkQ : (a : M) → M₂ ⧸ q) x : M₂ ⧸ q)

Tactic:
simp
-- 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
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
R₃ : Type u_5
M₃ : Type u_6
inst_6 : Ring R₃
inst_7 : AddCommGroup M₃
inst_8 : Module R₃ M₃
p₂ : Submodule R₂ M₂
p₃ : Submodule R₃ M₃
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
hf : p ≤ comap f p₂
hg : p₂ ≤ comap g p₃
h : p ≤ comap f (comap g p₃)
h₁ :
  ∀ (x : M),
    Eq.{u_6 + 1} (α := M₃ ⧸ p₃) ((p.mapQ p₃ (g ∘ₛₗ f) h ∘ₛₗ p.mkQ : (a : M) → M₃ ⧸ p₃) x : M₃ ⧸ p₃)
      (((p₂.mapQ p₃ g hg ∘ₛₗ p.mapQ p₂ f hf) ∘ₛₗ p.mkQ : (a : M) → M₃ ⧸ p₃) x : M₃ ⧸ p₃)
⊢ p.mapQ p₃ (g ∘ₛₗ f) h = p₂.mapQ p₃ g hg ∘ₛₗ p.mapQ p₂ 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
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₂
R₃ : Type u_5
M₃ : Type u_6
inst_6 : Ring R₃
inst_7 : AddCommGroup M₃
inst_8 : Module R₃ M₃
p₂ : Submodule R₂ M₂
p₃ : Submodule R₃ M₃
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
hf : p ≤ comap f p₂
hg : p₂ ≤ comap g p₃
h : p ≤ comap f (comap g p₃)
x : M
⊢ Eq.{u_6 + 1} (α := M₃ ⧸ p₃) ((p.mapQ p₃ (g ∘ₛₗ f) h ∘ₛₗ p.mkQ : (a : M) → M₃ ⧸ p₃) x : M₃ ⧸ p₃)
    (((p₂.mapQ p₃ g hg ∘ₛₗ p.mapQ p₂ f hf) ∘ₛₗ p.mkQ : (a : M) → M₃ ⧸ p₃) x : M₃ ⧸ p₃)

Tactic:
simp
-- 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'' : 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₂
rw rw₁ : p ≤ p
⊢ p ≤ comap LinearMap.id p

Tactic:
rw [comap_id]

Premises used: Submodule.comap_id
-- 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
h : p ≤ comap LinearMap.id p
h₁ :
  ∀ (x : M),
    Eq (α := M ⧸ p) ((p.mapQ p LinearMap.id h ∘ₗ p.mkQ : (a : M) → M ⧸ p) x : M ⧸ p)
      ((LinearMap.id ∘ₗ p.mkQ : (a : M) → M ⧸ p) x : M ⧸ p)
⊢ p.mapQ p LinearMap.id h = LinearMap.id

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
p : Submodule R M
h : p ≤ comap LinearMap.id p
x : M
⊢ Eq (α := M ⧸ p) ((p.mapQ p LinearMap.id h ∘ₗ p.mkQ : (a : M) → M ⧸ p) x : M ⧸ p)
    ((LinearMap.id ∘ₗ p.mkQ : (a : M) → M ⧸ p) x : M ⧸ p)

Tactic:
simp
-- 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
f : M →ₗ[R] M
h : p ≤ comap f p
h' : p ≤ comap (HPow.hPow (β := ℕ) f 0) p
⊢ p.mapQ p (HPow.hPow (β := ℕ) f 0) h' = HPow.hPow (β := ℕ) (p.mapQ p f h) 0

Tactic:
simp [Module.End.one_eq_id]

Premises used: Module.End.one_eq_id
-- 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
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : ∀ (h' : p ≤ comap (f ^ k) p), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
h' : p ≤ comap (f ^ (k + 1)) p
succ : p.mapQ p ((f ^ k) ∘ₗ f) ⋯ = (p.mapQ p f h ^ k) ∘ₗ p.mapQ p f h
⊢ p.mapQ p (f ^ (k + 1)) h' = p.mapQ p f h ^ (k + 1)

Tactic:
simp only [Module.End.iterate_succ]

Premises used: Module.End.iterate_succ
-- 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
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : ∀ (h' : p ≤ comap (f ^ k) p), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
h' : p ≤ comap (f ^ (k + 1)) p
succ : p ≤ comap (f ^ k) p
⊢ p.mapQ p ((f ^ k) ∘ₗ f) ⋯ = (p.mapQ p f h ^ k) ∘ₗ p.mapQ p f h

Tactic:
rw [mapQ_comp, ih]

Premises used: Submodule.comap_mono, LE.le.trans, Submodule.mapQ_comp
-- 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
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : ∀ (h' : p ≤ comap (f ^ k) p), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
h' : p ≤ comap (f ^ (k + 1)) p
⊢ p ≤ comap (f ^ k) p

Tactic:
p.le_comap_pow_of_le_comap h k

Premises used: Set.Mem, Submodule.le_comap_pow_of_le_comap
-- 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
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : ∀ (h' : p ≤ comap (f ^ k) p), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
h' : p ≤ comap (f ^ (k + 1)) p
⊢ p ≤ comap (f ^ k) p

Tactic:
exact p.le_comap_pow_of_le_comap h k

Premises used: Submodule.le_comap_pow_of_le_comap
-- 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
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
h' : p ≤ comap (f ^ k) p
zero :
  ∀ (h' : p ≤ comap (HPow.hPow (β := ℕ) f 0) p),
    p.mapQ p (HPow.hPow (β := ℕ) f 0) h' = HPow.hPow (β := ℕ) (p.mapQ p f h) 0
succ :
  ∀ (k : ℕ) (ih : ∀ (h' : p ≤ comap (f ^ k) p), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k)
    (h' : p ≤ comap (f ^ (k + 1)) p), p.mapQ p (f ^ (k + 1)) h' = p.mapQ p f h ^ (k + 1)
⊢ p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k

Tactic:
induction k with
  | zero => simp [Module.End.one_eq_id]
  | succ k ih =>
    simp only [Module.End.iterate_succ]
    rw [mapQ_comp, ih]
    exact p.le_comap_pow_of_le_comap h k

Premises used: Submodule.comap_mono, Module.End.one_eq_id, Submodule.zero, LE.le.trans, Submodule.mapQ_comp, Module.End.iterate_succ, Submodule.le_comap_pow_of_le_comap
-- 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
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₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
x_1 : M ⧸ p
x : M
hx : Quot.mk (⇑p.quotientRel : M → M → Prop) x ∈ comap (p.liftQ f h) q
⊢ Quot.mk (⇑p.quotientRel : M → M → Prop) x ∈ map p.mkQ (comap f q)

Tactic:
⟨_, hx, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, 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
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₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
x_1 : M ⧸ p
x : M
hx : Quot.mk (⇑p.quotientRel : M → M → Prop) x ∈ comap (p.liftQ f h) q
⊢ Quot.mk (⇑p.quotientRel : M → M → Prop) x ∈ map p.mkQ (comap f q)

Tactic:
exact ⟨_, hx, 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
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₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
rw : comap f q ≤ comap p.mkQ (comap (p.liftQ f h) q)
rw₁ : comap f q ≤ comap (p.liftQ f h ∘ₛₗ p.mkQ) q
rw₂ rw₃ : comap f q ≤ comap f q
⊢ map p.mkQ (comap f q) ≤ comap (p.liftQ f h) q

Tactic:
rw [map_le_iff_le_comap, ← comap_comp, liftQ_mkQ]

Premises used: Submodule.comap_comp, Submodule.map_le_iff_le_comap, Submodule.liftQ_mkQ
-- 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
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₂
h : p ≤ f.ker
q : Submodule R (M ⧸ p)
w : M ⧸ p
x : M
hxq : Quot.mk (⇑p.quotientRel : M → M → Prop) x ∈ (↑q : Set (M ⧸ p))
⊢ Membership.mem (α := M₂) (map f (comap p.mkQ q))
    ((p.liftQ f h : (a : M ⧸ p) → M₂) (Quot.mk (⇑p.quotientRel : M → M → Prop) x) : M₂)

Tactic:
⟨x, hxq, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, 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
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₂
h : p ≤ f.ker
q : Submodule R (M ⧸ p)
w : M ⧸ p
x : M
hxq : Quot.mk (⇑p.quotientRel : M → M → Prop) x ∈ (↑q : Set (M ⧸ p))
⊢ Membership.mem (α := M₂) (map f (comap p.mkQ q))
    ((p.liftQ f h : (a : M ⧸ p) → M₂) (Quot.mk (⇑p.quotientRel : M → M → Prop) x) : M₂)

Tactic:
exact ⟨x, hxq, 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
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₂
h : p ≤ f.ker
q : Submodule R (M ⧸ p)
x : M
hxq : x ∈ (↑(comap p.mkQ q) : Set M)
⊢ Membership.mem (α := M₂) (map (p.liftQ f h) q) ((f : (a : M) → M₂) x : M₂)

Tactic:
⟨Quotient.mk x, hxq, rfl⟩

Premises used: Set.Mem, Submodule.Quotient.mk, setOf, And.intro, Exists.intro, Set.image, 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
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₂
h : p ≤ f.ker
q : Submodule R (M ⧸ p)
x : M
hxq : x ∈ (↑(comap p.mkQ q) : Set M)
⊢ Membership.mem (α := M₂) (map (p.liftQ f h) q) ((f : (a : M) → M₂) x : M₂)

Tactic:
exact ⟨Quotient.mk x, hxq, 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
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
⊢ (p.liftQ f h).ker = map p.mkQ f.ker

Tactic:
comap_liftQ _ _ _ _

Premises used: LinearMap.ker, Submodule.comap_liftQ
-- 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
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₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
⊢ (p.mapQ q f h).ker = map p.mkQ (comap f q)

Tactic:
simp [Submodule.mapQ, Submodule.ker_liftQ, LinearMap.ker_comp]

Premises used: LinearMap.ker_comp, Submodule.mapQ, Submodule.ker_liftQ
-- 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
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₂
h : p ≤ f.ker
⊢ (p.liftQ f h).range = f.range

Tactic:
simpa only [range_eq_map] using map_liftQ _ _ _ _

Premises used: Submodule.map_liftQ, LinearMap.range_eq_map
-- 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
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 = ⊥
rw₂ rw₃ : Eq.{u_2 + 1} (α := Submodule R (M ⧸ f.ker)) ⊥ ⊥
⊢ (p.liftQ f h).ker = ⊥

Tactic:
rw [ker_liftQ, le_antisymm h h', mkQ_map_self]

Premises used: le_antisymm, Submodule.mkQ_map_self, Submodule.ker_liftQ
-- 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
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
⊢ (p.liftQ f ⋯).ker = ⊥

Tactic:
ker_liftQ_eq_bot p f h.le h.ge

Premises used: Eq.ge, Eq.le, Submodule.ker_liftQ_eq_bot
-- 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
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
rw₂ rw₃ : map q.mkQ f.range = map q.mkQ f.range
⊢ (p.mapQ q f h).range = map q.mkQ f.range

Tactic:
rw [mapQ, range_liftQ, range_comp]

Premises used: LinearMap.range_comp, Submodule.mapQ, Submodule.range_liftQ
-- 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 p' : Submodule R M
H : p ≤ p'
x : M
⊢ 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:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, 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 p' : Submodule R M
H : p ≤ p'
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')
⊢ factor H ∘ₗ p.mkQ = p'.mkQ

Tactic:
ext x
-- 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 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')
h₁ h₂ : Eq (α := 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')

Tactic:
rw [LinearMap.comp_apply, factor_mk]

Premises used: Submodule.factor_mk, LinearMap.comp_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
p p' p'' : Submodule R M
H1 : p ≤ p'
H2 : p' ≤ p''
h :
  ∀ (x : M),
    Eq (α := M ⧸ p'') (((factor H2 ∘ₗ factor H1) ∘ₗ p.mkQ : (a : M) → M ⧸ p'') x : M ⧸ p'')
      ((factor ⋯ ∘ₗ p.mkQ : (a : M) → M ⧸ p'') x : M ⧸ p'')
⊢ factor H2 ∘ₗ factor H1 = factor ⋯

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
p p' p'' : Submodule R M
H1 : p ≤ p'
H2 : p' ≤ p''
x : M
⊢ Eq (α := M ⧸ p'') (((factor H2 ∘ₗ factor H1) ∘ₗ p.mkQ : (a : M) → M ⧸ p'') x : M ⧸ p'')
    ((factor ⋯ ∘ₗ p.mkQ : (a : M) → M ⧸ p'') x : M ⧸ p'')

Tactic:
simp
-- 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 p' p'' : Submodule R M
H1 : p ≤ p'
H2 : p' ≤ p''
x : M ⧸ p
rw :
  Eq (α := M ⧸ p'') ((factor H2 ∘ₗ factor H1 : (a : M ⧸ p) → M ⧸ p'') x : M ⧸ p'')
    ((factor ⋯ : (a : M ⧸ p) → M ⧸ 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'')

Tactic:
rw [← comp_apply]

Premises used: LinearMap.comp_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
p p' p'' : Submodule R M
H1 : p ≤ p'
H2 : p' ≤ p''
x : M ⧸ p
⊢ Eq (α := M ⧸ p'') ((factor H2 ∘ₗ factor H1 : (a : M ⧸ p) → M ⧸ p'') x : M ⧸ p'')
    ((factor ⋯ : (a : M ⧸ p) → M ⧸ p'') x : M ⧸ p'')

Tactic:
simp
-- 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 p' : Submodule R M
H : p ≤ p'
x : M ⧸ p'
h : (factor H : (a : M ⧸ p) → M ⧸ p') (Quotient.mk (Quotient.out x)) = x
⊢ ∃ (a : M ⧸ p), (factor H : (a : M ⧸ p) → M ⧸ p') a = x

Tactic:
use Quotient.mk x.out

Premises used: Submodule.Quotient.mk, Quotient.out
-- 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 p' : Submodule R M
H : p ≤ p'
x : M ⧸ p'
⊢ (factor H : (a : M ⧸ p) → M ⧸ p') (Quotient.mk (Quotient.out x)) = x

Tactic:
Quotient.out_eq x

Premises used: Quot.out, Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, Quotient.out, Classical.choose, Quotient.out_eq
-- 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 p' : Submodule R M
H : p ≤ p'
x : M ⧸ p'
⊢ (factor H : (a : M ⧸ p) → M ⧸ p') (Quotient.mk (Quotient.out x)) = x

Tactic:
exact Quotient.out_eq x

Premises used: Quotient.out_eq
-- 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'_1 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₂
p' : Submodule R (M ⧸ p)
⊢ p' ≤ p.mkQ.range

Tactic:
simp
-- 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'' : 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_1 : Submodule R₂ M₂
x_1 : (↑(Set.Ici p) : Type u_2)
q : Submodule R M
hq : q ∈ Set.Ici p
⊢ (↑((fun (p' : Submodule R (M ⧸ p)) ↦ Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ Set.Ici p) (comap p.mkQ p') ⋯)
          ((fun (q : (↑(Set.Ici p) : Type u_2)) ↦ map p.mkQ (↑q : Submodule R M))
            (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ Set.Ici p) q hq))) :
      Submodule R M) =
    (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ Set.Ici p) q hq) : Submodule R M)

Tactic:
simpa [comap_map_mkQ p]

Premises used: Submodule.comap_map_mkQ
-- 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
p' : Submodule R (M ⧸ p)
⊢ (p.comapMkQOrderEmbedding : (a : Submodule R (M ⧸ p)) → Submodule R M) p' = comap p.mkQ p'

Tactic:
rfl

Premises used: Submodule.comap, 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
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₂)
this : comap f (span R₂ s) ≤ span R ((⇑f : (a : M) → M₂) ⁻¹' s)
⊢ span R ((⇑f : (a : M) → M₂) ⁻¹' s) = comap f (span R₂ s)

Tactic:
le_antisymm (span_preimage_le f s) this

Premises used: le_antisymm, Submodule.span_preimage_le
-- 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₂)
this : comap f (span R₂ s) ≤ span R ((⇑f : (a : M) → M₂) ⁻¹' s)
⊢ span R ((⇑f : (a : M) → M₂) ⁻¹' s) = comap f (span R₂ s)

Tactic:
exact le_antisymm (span_preimage_le f s) this

Premises used: le_antisymm, Submodule.span_preimage_le
-- 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₂)
suffices : comap f (span R₂ s) ≤ span R ((⇑f : (a : M) → M₂) ⁻¹' s)
⊢ span R ((⇑f : (a : M) → M₂) ⁻¹' s) = comap f (span R₂ s)

Tactic:
suffices (span R₂ s).comap f ≤ span R (f ⁻¹' s) by exact le_antisymm (span_preimage_le f s) this