-- Mathlib/Algebra/Module/Presentation/Basic.lean
lemma postcomp_injective {f f' : M →ₗ[A] N}
    (h' : solution.postcomp f = solution.postcomp f') : f = f'

Proof state:
case h.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 : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
this : f ∘ₗ solution.fromQuotient = f' ∘ₗ solution.fromQuotient
y : relations.Quotient
⊢ f (solution.fromQuotient y) = f' (solution.fromQuotient y)

Tactic:
exact DFunLike.congr_fun this y

Result:
no goals

Proof state:
case h
A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
g : relations.G
⊢ (f ∘ₗ solution.fromQuotient) (relations.toQuotient (Finsupp.single g 1)) =
    (f' ∘ₗ solution.fromQuotient) (relations.toQuotient (Finsupp.single g 1))

Tactic:
simpa using congr_var h' g

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
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
⊢ f ∘ₗ solution.fromQuotient = f' ∘ₗ solution.fromQuotient

Tactic:
ext g

Result:
case h
A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
g : relations.G
⊢ (f ∘ₗ solution.fromQuotient) (relations.toQuotient (Finsupp.single g 1)) =
    (f' ∘ₗ solution.fromQuotient) (relations.toQuotient (Finsupp.single g 1))

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 : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
this : f ∘ₗ solution.fromQuotient = f' ∘ₗ solution.fromQuotient
⊢ f = f'

Tactic:
ext x

Result:
case h
A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
this : f ∘ₗ solution.fromQuotient = f' ∘ₗ solution.fromQuotient
x : M
⊢ f x = f' 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 : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
⊢ f = f'

Tactic:
suffices f.comp solution.fromQuotient = f'.comp solution.fromQuotient by
  ext x
  obtain ⟨y, rfl⟩ := h.bijective.2 x
  exact DFunLike.congr_fun this y

Result:
A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
⊢ f ∘ₗ solution.fromQuotient = f' ∘ₗ solution.fromQuotient

Proof state:
case h
A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
this : f ∘ₗ solution.fromQuotient = f' ∘ₗ solution.fromQuotient
x : M
⊢ f x = f' x

Tactic:
obtain ⟨y, rfl⟩ := h.bijective.2 x

Result:
case h.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 : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
this : f ∘ₗ solution.fromQuotient = f' ∘ₗ solution.fromQuotient
y : relations.Quotient
⊢ f (solution.fromQuotient y) = f' (solution.fromQuotient y)