-- Mathlib/Algebra/Exact.lean
lemma ker_eq_bot_range_liftQ_iff (h : range f ≤ ker g) :
    ker ((range f).liftQ g h) = ⊥ ↔ ker g = range f

Proof state:
case mpr
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : range f ≤ ker g
⊢ (∀ (x : N), g x = 0 ↔ ∃ y, f y = x) → ∀ (x : N ⧸ range f), ((range f).liftQ g h) x = 0 ↔ x = 0

Tactic:
intro hfg x

Result:
case mpr
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : range f ≤ ker g
hfg : ∀ (x : N), g x = 0 ↔ ∃ y, f y = x
x : N ⧸ range f
⊢ ((range f).liftQ g h) x = 0 ↔ x = 0

Proof state:
case mpr.intro
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : range f ≤ ker g
hfg : ∀ (x : N), g x = 0 ↔ ∃ y, f y = x
x : N
⊢ ((range f).liftQ g h) (Submodule.Quotient.mk x) = 0 ↔ Submodule.Quotient.mk x = 0

Tactic:
simpa using hfg x

Result:
no goals

Proof state:
case mp
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : range f ≤ ker g
⊢ (∀ (x : N ⧸ range f), ((range f).liftQ g h) x = 0 ↔ x = 0) → ∀ (x : N), g x = 0 ↔ ∃ y, f y = x

Tactic:
intro hfg x

Result:
case mp
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : range f ≤ ker g
hfg : ∀ (x : N ⧸ range f), ((range f).liftQ g h) x = 0 ↔ x = 0
x : N
⊢ g x = 0 ↔ ∃ y, f y = x

Proof state:
case mp
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : range f ≤ ker g
hfg : ∀ (x : N ⧸ range f), ((range f).liftQ g h) x = 0 ↔ x = 0
x : N
⊢ g x = 0 ↔ ∃ y, f y = x

Tactic:
simpa using hfg (Submodule.Quotient.mk x)

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : range f ≤ ker g
⊢ ker ((range f).liftQ g h) = ⊥ ↔ ker g = range f

Tactic:
simp only [Submodule.ext_iff, mem_ker, Submodule.mem_bot, mem_range]

Result:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : range f ≤ ker g
⊢ (∀ (x : N ⧸ range f), ((range f).liftQ g h) x = 0 ↔ x = 0) ↔ ∀ (x : N), g x = 0 ↔ ∃ y, f y = x

Proof state:
case mpr
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : range f ≤ ker g
hfg : ∀ (x : N), g x = 0 ↔ ∃ y, f y = x
x : N ⧸ range f
⊢ ((range f).liftQ g h) x = 0 ↔ x = 0

Tactic:
obtain ⟨x, rfl⟩ := Submodule.Quotient.mk_surjective _ x

Result:
case mpr.intro
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : range f ≤ ker g
hfg : ∀ (x : N), g x = 0 ↔ ∃ y, f y = x
x : N
⊢ ((range f).liftQ g h) (Submodule.Quotient.mk x) = 0 ↔ Submodule.Quotient.mk x = 0

Proof state:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : range f ≤ ker g
⊢ (∀ (x : N ⧸ range f), ((range f).liftQ g h) x = 0 ↔ x = 0) ↔ ∀ (x : N), g x = 0 ↔ ∃ y, f y = x

Tactic:
constructor

Result:
case mp
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : range f ≤ ker g
⊢ (∀ (x : N ⧸ range f), ((range f).liftQ g h) x = 0 ↔ x = 0) → ∀ (x : N), g x = 0 ↔ ∃ y, f y = x

case mpr
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : range f ≤ ker g
⊢ (∀ (x : N), g x = 0 ↔ ∃ y, f y = x) → ∀ (x : N ⧸ range f), ((range f).liftQ g h) x = 0 ↔ x = 0