-- Mathlib/Algebra/Module/Presentation/Basic.lean
lemma injective_fromQuotient_iff_ker_π_eq_span :
    Function.Injective solution.fromQuotient ↔
      LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)

Proof state:
case mpr.intro
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)
x : relations.G →₀ A
hx : x ∈ LinearMap.ker solution.π
⊢ relations.toQuotient x ∈ ⊥

Tactic:
rw [h, ← range_map] at hx

Result:
case mpr.intro
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)
x : relations.G →₀ A
hx : x ∈ LinearMap.range relations.map
⊢ relations.toQuotient x ∈ ⊥

Proof state:
case mpr
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
⊢ LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation) → Function.Injective ⇑solution.fromQuotient

Tactic:
intro h

Result:
case mpr
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)
⊢ Function.Injective ⇑solution.fromQuotient

Proof state:
case mpr.intro.intro
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)
x : relations.R →₀ A
⊢ relations.toQuotient (relations.map x) ∈ ⊥

Tactic:
simp only [toQuotient_map_apply, Submodule.zero_mem]

Result:
no goals

Proof state:
case mpr
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)
⊢ Function.Injective ⇑solution.fromQuotient

Tactic:
rw [← LinearMap.ker_eq_bot, eq_bot_iff]

Result:
case mpr
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)
⊢ LinearMap.ker solution.fromQuotient ≤ ⊥

Proof state:
case mpr
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)
x : relations.Quotient
hx : x ∈ LinearMap.ker solution.fromQuotient
⊢ x ∈ ⊥

Tactic:
obtain ⟨x, rfl⟩ := relations.surjective_toQuotient x

Result:
case mpr.intro
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)
x : relations.G →₀ A
hx : relations.toQuotient x ∈ LinearMap.ker solution.fromQuotient
⊢ relations.toQuotient x ∈ ⊥

Proof state:
case mp
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
⊢ Function.Injective ⇑solution.fromQuotient → LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)

Tactic:
intro h

Result:
case mp
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : Function.Injective ⇑solution.fromQuotient
⊢ LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)

Proof state:
case mpr
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)
⊢ LinearMap.ker solution.fromQuotient ≤ ⊥

Tactic:
intro x hx

Result:
case mpr
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)
x : relations.Quotient
hx : x ∈ LinearMap.ker solution.fromQuotient
⊢ x ∈ ⊥

Proof state:
case mpr.intro
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)
x : relations.G →₀ A
hx : x ∈ LinearMap.range relations.map
⊢ relations.toQuotient x ∈ ⊥

Tactic:
obtain ⟨x, rfl⟩ := hx

Result:
case mpr.intro.intro
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)
x : relations.R →₀ A
⊢ relations.toQuotient (relations.map x) ∈ ⊥

Proof state:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)
x : relations.G →₀ A
hx : relations.toQuotient x ∈ LinearMap.ker solution.fromQuotient
⊢ x ∈ LinearMap.ker solution.π

Tactic:
simpa only [LinearMap.mem_ker, fromQuotient_toQuotient] using hx

Result:
no goals

Proof state:
case mpr.intro
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)
x : relations.G →₀ A
hx : relations.toQuotient x ∈ LinearMap.ker solution.fromQuotient
⊢ relations.toQuotient x ∈ ⊥

Tactic:
replace hx : x ∈ LinearMap.ker solution.π := by
  simpa only [LinearMap.mem_ker, fromQuotient_toQuotient] using hx

Result:
case mpr.intro
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)
x : relations.G →₀ A
hx : x ∈ LinearMap.ker solution.π
⊢ relations.toQuotient x ∈ ⊥

Proof state:
case mp
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : Function.Injective ⇑solution.fromQuotient
⊢ LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)

Tactic:
rw [← ker_toQuotient, ← fromQuotient_comp_toQuotient, LinearMap.ker_comp,
  LinearMap.ker_eq_bot.2 h, Submodule.comap_bot]

Result:
no goals

Proof state:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
⊢ Function.Injective ⇑solution.fromQuotient ↔ LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)

Tactic:
constructor

Result:
case mp
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
⊢ Function.Injective ⇑solution.fromQuotient → LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)

case mpr
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
⊢ LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation) → Function.Injective ⇑solution.fromQuotient